1  /-
  2  Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel
  5  Adapted from the corresponding theory for complete lattices.
  6  
  7  Theory of conditionally complete lattices.
  8  
  9  A conditionally complete lattice is a lattice in which every non-empty bounded subset s
 10  has a least upper bound and a greatest lower bound, denoted below by Sup s and Inf s.
 11  Typical examples are real, nat, int with their usual orders.
 12  
 13  The theory is very comparable to the theory of complete lattices, except that suitable
 14  boundedness and nonemptiness assumptions have to be added to most statements.
 15  We introduce two predicates bdd_above and bdd_below to express this boundedness, prove
 16  their basic properties, and then go on to prove most useful properties of Sup and Inf
 17  in conditionally complete lattices.
 18  
 19  To differentiate the statements between complete lattices and conditionally complete
 20  lattices, we prefix Inf and Sup in the statements by c, giving cInf and cSup. For instance,
 21  Inf_le is a statement in complete lattices ensuring Inf s ≤ x, while cInf_le is the same
 22  statement in conditionally complete lattices with an additional assumption that s is
 23  bounded below.
 24  -/
 25  import
 26    order.lattice order.complete_lattice order.bounds
src    └───────────┘ └────────────────────┘ └──────────┘
 27    tactic.finish data.set.finite
src    └───────────┘ └─────────────┘
 28  
 29  set_option old_structure_cmd true
doc             └───────────────┘
 30  
 31  open set lattice
 32  
 33  universes u v w
 34  variables {α : Type u} {β : Type v} {ι : Sort w}
 35  
 36  
 37  section
 38  
 39  /-!
 40  Extension of Sup and Inf from a preorder `α` to `with_top α` and `with_bot α`
 41  -/
 42  
 43  open_locale classical
 44  
 45  noncomputable instance {α : Type*} [preorder α] [has_Sup α] : has_Sup (with_top α) :=
id                                       └──────┘    └─────┘     └─────┘  └──────┘ 
src                                      └──────┘     └─────┘      └─────┘  └──────┘
typ                                      └──────┘    └─────┘     └─────┘  └──────┘ 
doc                                                   └─────┘      └─────┘
 46  ⟨λ S, if ⊤ ∈ S then ⊤ else
id                   
src                    
typ                  
 47    if bdd_above (coe ⁻¹' S : set α) then ↑(Sup (coe ⁻¹' S : set α)) else ⊤⟩
id        └───────┘  └─┘ └─┘    └─┘         └─┘  └─┘ └─┘    └─┘         
src       └───────┘  └─┘ └─┘     └─┘          └─┘  └─┘ └─┘     └─┘          
typ       └───────┘  └─┘ └─┘    └─┘         └─┘  └─┘ └─┘    └─┘         
doc       └───────┘      └─┘                   └─┘      └─┘
 48  
 49  noncomputable instance {α : Type*} [has_Inf α] : has_Inf (with_top α) :=
id                                       └─────┘     └─────┘  └──────┘ 
src                                      └─────┘      └─────┘  └──────┘
typ                                      └─────┘     └─────┘  └──────┘ 
doc                                      └─────┘      └─────┘
 50  ⟨λ S, if S ⊆ {⊤} then ⊤ else ↑(Inf (coe ⁻¹' S : set α))⟩
id                           └─┘  └─┘ └─┘    └─┘ 
src                            └─┘  └─┘ └─┘     └─┘
typ                          └─┘  └─┘ └─┘    └─┘ 
doc                                 └─┘      └─┘
 51  
 52  noncomputable instance {α : Type*} [has_Sup α] : has_Sup (with_bot α) :=
id                                       └─────┘     └─────┘  └──────┘ 
src                                      └─────┘      └─────┘  └──────┘
typ                                      └─────┘     └─────┘  └──────┘ 
doc                                      └─────┘      └─────┘
 53  ⟨(@with_top.lattice.has_Inf (order_dual α) _).Inf⟩
id      └──────────────────────┘  └────────┘     └─┘
src     └──────────────────────┘  └────────┘      └─┘
typ     └──────────────────────┘  └────────┘     └─┘
doc                               └────────┘
 54  
 55  noncomputable instance {α : Type*} [preorder α] [has_Inf α] : has_Inf (with_bot α) :=
id                                       └──────┘    └─────┘     └─────┘  └──────┘ 
src                                      └──────┘     └─────┘      └─────┘  └──────┘
typ                                      └──────┘    └─────┘     └─────┘  └──────┘ 
doc                                                   └─────┘      └─────┘
 56  ⟨(@with_top.lattice.has_Sup (order_dual α) _ _).Sup⟩
id      └──────────────────────┘  └────────┘       └─┘
src     └──────────────────────┘  └────────┘        └─┘
typ     └──────────────────────┘  └────────┘       └─┘
doc                               └────────┘
 57  
 58  end -- section
 59  
 60  namespace lattice
 61  section prio
 62  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
 63  /-- A conditionally complete lattice is a lattice in which
 64  every nonempty subset which is bounded above has a supremum, and
 65  every nonempty subset which is bounded below has an infimum.
 66  Typical examples are real numbers or natural numbers.
 67  
 68  To differentiate the statements from the corresponding statements in (unconditional)
 69  complete lattices, we prefix Inf and Sup by a c everywhere. The same statements should
 70  hold in both worlds, sometimes with additional assumptions of nonemptiness or
 71  boundedness.-/
 72  class conditionally_complete_lattice (α : Type u) extends lattice α, has_Sup α, has_Inf α :=
id                                             └──┘            └─────┘   └─────┘   └─────┘ 
src                                                            └─────┘    └─────┘    └─────┘
typ                                            └──┘            └─────┘   └─────┘   └─────┘ 
doc                                                            └─────┘    └─────┘    └─────┘
 73  (le_cSup : ∀s a, bdd_above s → a ∈ s → a ≤ Sup s)
id                  └───────┘           └─┘ 
src                   └───────┘              
typ                 └───────┘           └─┘ 
doc                   └───────┘
 74  (cSup_le : ∀ s a, set.nonempty s → a ∈ upper_bounds s → Sup s ≤ a)
id                   └──────────┘      └──────────┘    └─┘   
src                    └──────────┘        └──────────┘           
typ                  └──────────┘      └──────────┘    └─┘   
doc                    └──────────┘         └──────────┘
 75  (cInf_le : ∀s a, bdd_below s → a ∈ s → Inf s ≤ a)
id                  └───────┘         └─┘   
src                   └───────┘                  
typ                 └───────┘         └─┘   
doc                   └───────┘
 76  (le_cInf : ∀s a, set.nonempty s → a ∈ lower_bounds s → a ≤ Inf s)
id                  └──────────┘      └──────────┘      └─┘ 
src                   └──────────┘        └──────────┘       
typ                 └──────────┘      └──────────┘      └─┘ 
doc                   └──────────┘         └──────────┘
 77  
 78  class conditionally_complete_linear_order (α : Type u)
id                                                  └──┘
typ                                                 └──┘
 79    extends conditionally_complete_lattice α, decidable_linear_order α
id             └────────────────────────────┘   └────────────────────┘ 
src            └────────────────────────────┘    └────────────────────┘
typ            └────────────────────────────┘   └────────────────────┘ 
doc            └────────────────────────────┘
 80  
 81  class conditionally_complete_linear_order_bot (α : Type u)
id                                                     └──┘
typ                                                    └──┘
 82    extends conditionally_complete_lattice α, decidable_linear_order α, order_bot α :=
id             └────────────────────────────┘   └────────────────────┘   └───────┘ 
src            └────────────────────────────┘    └────────────────────┘    └───────┘
typ            └────────────────────────────┘   └────────────────────┘   └───────┘ 
doc            └────────────────────────────┘                              └───────┘
 83  (cSup_empty : Sup ∅ = ⊥)
id                 └─┘   
src                      
typ                └─┘   
 84  end prio
 85  
 86  /- A complete lattice is a conditionally complete lattice, as there are no restrictions
 87  on the properties of Inf and Sup in a complete lattice.-/
 88  
 89  @[priority 100] -- see Note [lower instance priority]
 90  instance conditionally_complete_lattice_of_complete_lattice [complete_lattice α]:
id                                                                └──────────────┘ 
src                                                               └──────────────┘
typ                                                               └──────────────┘ 
doc                                                               └──────────────┘
 91    conditionally_complete_lattice α :=
id     └────────────────────────────┘ 
src    └────────────────────────────┘
typ    └────────────────────────────┘ 
doc    └────────────────────────────┘
 92  { le_cSup := by intros; apply le_Sup; assumption,
id                                 └────┘
src                  └────┘  └────┘└────┘  └────────┘
typ                  └────┘  └────┘└────┘  └────────┘
doc                  └────┘  └────┘        └────────┘
txt                  └────┘  └────┘        └────────┘
par                  └────┘  └────┘        └────────┘
pid                               
st                  └───────────────────────────────┘
 93    cSup_le := by intros; apply Sup_le; assumption,
id                                 └────┘
src                  └────┘  └────┘└────┘  └────────┘
typ                  └────┘  └────┘└────┘  └────────┘
doc                  └────┘  └────┘        └────────┘
txt                  └────┘  └────┘        └────────┘
par                  └────┘  └────┘        └────────┘
pid                               
st                  └───────────────────────────────┘
 94    cInf_le := by intros; apply Inf_le; assumption,
id                                 └────┘
src                  └────┘  └────┘└────┘  └────────┘
typ                  └────┘  └────┘└────┘  └────────┘
doc                  └────┘  └────┘        └────────┘
txt                  └────┘  └────┘        └────────┘
par                  └────┘  └────┘        └────────┘
pid                               
st                  └───────────────────────────────┘
 95    le_cInf := by intros; apply le_Inf; assumption,
id                                 └────┘
src                  └────┘  └────┘└────┘  └────────┘
typ                  └────┘  └────┘└────┘  └────────┘
doc                  └────┘  └────┘        └────────┘
txt                  └────┘  └────┘        └────────┘
par                  └────┘  └────┘        └────────┘
pid                               
st                  └───────────────────────────────┘
 96    ..‹complete_lattice α› }
id       └──────────────┘ 
src      └──────────────┘  
typ      └──────────────┘ 
doc      └──────────────┘  
 97  
 98  @[priority 100] -- see Note [lower instance priority]
 99  instance conditionally_complete_linear_order_of_complete_linear_order [complete_linear_order α]:
id                                                                          └───────────────────┘ 
src                                                                         └───────────────────┘
typ                                                                         └───────────────────┘ 
doc                                                                         └───────────────────┘
100    conditionally_complete_linear_order α :=
id     └─────────────────────────────────┘ 
src    └─────────────────────────────────┘
typ    └─────────────────────────────────┘ 
101  { ..lattice.conditionally_complete_lattice_of_complete_lattice, .. ‹complete_linear_order α› }
id       └────────────────────────────────────────────────────────┘     └───────────────────┘ 
src      └────────────────────────────────────────────────────────┘     └───────────────────┘  
typ      └────────────────────────────────────────────────────────┘     └───────────────────┘ 
doc                                                                     └───────────────────┘  
102  
103  section conditionally_complete_lattice
104  variables [conditionally_complete_lattice α] {s t : set α} {a b : α}
id              └────────────────────────────┘           └─┘
src             └────────────────────────────┘           └─┘
typ             └────────────────────────────┘           └─┘
doc             └────────────────────────────┘
105  
106  theorem le_cSup (h₁ : bdd_above s) (h₂ : a ∈ s) : a ≤ Sup s :=
id                         └───────┘                 └─┘ 
src                        └───────┘                     └─┘
typ                        └───────┘                 └─┘ 
doc                        └───────┘                       └─┘
107  conditionally_complete_lattice.le_cSup s a h₁ h₂
id   └────────────────────────────────────┘   └┘ └┘
src  └────────────────────────────────────┘
typ  └────────────────────────────────────┘   └┘ └┘
108  
109  theorem cSup_le (h₁ : s.nonempty) (h₂ : ∀b∈s, b ≤ a) : Sup s ≤ a :=
id                         └───────┘                  └─┘   
src                         └───────┘                     └─┘   
typ                        └───────┘                  └─┘   
doc                         └───────┘                       └─┘
110  conditionally_complete_lattice.cSup_le s a h₁ h₂
id   └────────────────────────────────────┘   └┘ └┘
src  └────────────────────────────────────┘
typ  └────────────────────────────────────┘   └┘ └┘
111  
112  theorem cInf_le (h₁ : bdd_below s) (h₂ : a ∈ s) : Inf s ≤ a :=
id                         └───────┘               └─┘   
src                        └───────┘                  └─┘   
typ                        └───────┘               └─┘   
doc                        └───────┘                   └─┘
113  conditionally_complete_lattice.cInf_le s a h₁ h₂
id   └────────────────────────────────────┘   └┘ └┘
src  └────────────────────────────────────┘
typ  └────────────────────────────────────┘   └┘ └┘
114  
115  theorem le_cInf (h₁ : s.nonempty) (h₂ : ∀b∈s, a ≤ b) : a ≤ Inf s :=
id                         └───────┘                    └─┘ 
src                         └───────┘                         └─┘
typ                        └───────┘                    └─┘ 
doc                         └───────┘                           └─┘
116  conditionally_complete_lattice.le_cInf s a h₁ h₂
id   └────────────────────────────────────┘   └┘ └┘
src  └────────────────────────────────────┘
typ  └────────────────────────────────────┘   └┘ └┘
117  
118  theorem le_cSup_of_le (_ : bdd_above s) (hb : b ∈ s) (h : a ≤ b) : a ≤ Sup s :=
id                              └───────┘                          └─┘ 
src                             └───────┘                                └─┘
typ                             └───────┘                          └─┘ 
doc                             └───────┘                                   └─┘
119  le_trans h (le_cSup ‹bdd_above s› hb)
id   └──────┘   └─────┘ └───────┘  └┘
src  └──────┘    └─────┘ └───────┘  
typ  └──────┘   └─────┘ └───────┘  └┘
doc                      └───────┘  
120  
121  theorem cInf_le_of_le (_ : bdd_below s) (hb : b ∈ s) (h : b ≤ a) : Inf s ≤ a :=
id                              └───────┘                        └─┘   
src                             └───────┘                             └─┘   
typ                             └───────┘                        └─┘   
doc                             └───────┘                               └─┘
122  le_trans (cInf_le ‹bdd_below s› hb) h
id   └──────┘  └─────┘ └───────┘  └┘  
src  └──────┘  └─────┘ └───────┘  
typ  └──────┘  └─────┘ └───────┘  └┘  
doc                    └───────┘  
123  
124  theorem cSup_le_cSup (_ : bdd_above t) (_ : s.nonempty) (h : s ⊆ t) : Sup s ≤ Sup t :=
id                             └───────┘        └───────┘             └─┘   └─┘ 
src                            └───────┘          └───────┘               └─┘    └─┘
typ                            └───────┘        └───────┘             └─┘   └─┘ 
doc                            └───────┘          └───────┘                └─┘     └─┘
125  cSup_le ‹_› (assume (a) (ha : a ∈ s), le_cSup ‹bdd_above t› (h ha))
id   └─────┘                         └─────┘ └───────┘    └┘
src  └─────┘                            └─────┘ └───────┘  
typ  └─────┘                         └─────┘ └───────┘    └┘
doc                                              └───────┘  
126  
127  theorem cInf_le_cInf (_ : bdd_below t) (_ : s.nonempty) (h : s ⊆ t) : Inf t ≤ Inf s :=
id                             └───────┘        └───────┘             └─┘   └─┘ 
src                            └───────┘          └───────┘               └─┘    └─┘
typ                            └───────┘        └───────┘             └─┘   └─┘ 
doc                            └───────┘          └───────┘                └─┘     └─┘
128  le_cInf ‹_› (assume (a) (ha : a ∈ s), cInf_le ‹bdd_below t› (h ha))
id   └─────┘                         └─────┘ └───────┘    └┘
src  └─────┘                            └─────┘ └───────┘  
typ  └─────┘                         └─────┘ └───────┘    └┘
doc                                              └───────┘  
129  
130  theorem cSup_le_iff (_ : bdd_above s) (_ : s.nonempty) : Sup s ≤ a ↔ (∀b ∈ s, b ≤ a) :=
id                            └───────┘        └───────┘    └─┘              
src                           └───────┘          └───────┘    └─┘                  
typ                           └───────┘        └───────┘    └─┘              
doc                           └───────┘          └───────┘    └─┘
131  ⟨assume (_ : Sup s ≤ a) (b) (_ : b ∈ s),
id                └─┘               
src               └─┘                  
typ               └─┘               
doc               └─┘
132    le_trans (le_cSup ‹bdd_above s› ‹b ∈ s›) ‹Sup s ≤ a›,
id     └──────┘  └─────┘ └───────┘      └─┘   
src    └──────┘  └─────┘ └───────┘         └─┘     
typ    └──────┘  └─────┘ └───────┘      └─┘   
doc                      └───────┘          └─┘      
133    cSup_le ‹_›⟩
id     └─────┘  
src    └─────┘  
typ    └─────┘  
doc             
134  
135  theorem le_cInf_iff (_ : bdd_below s) (_ : s.nonempty) : a ≤ Inf s ↔ (∀b ∈ s, a ≤ b) :=
id                            └───────┘        └───────┘      └─┘            
src                           └───────┘          └───────┘       └─┘               
typ                           └───────┘        └───────┘      └─┘            
doc                           └───────┘          └───────┘        └─┘
136  ⟨assume (_ : a ≤ Inf s) (b) (_ : b ∈ s),
id                  └─┘             
src                  └─┘               
typ                 └─┘             
doc                   └─┘
137    le_trans ‹a ≤ Inf s› (cInf_le ‹bdd_below s› ‹b ∈ s›),
id     └──────┘   └─┘   └─────┘ └───────┘    
src    └──────┘    └─┘    └─────┘ └───────┘       
typ    └──────┘   └─┘   └─────┘ └───────┘    
doc                 └─┘            └───────┘        
138    le_cInf ‹_›⟩
id     └─────┘  
src    └─────┘  
typ    └─────┘  
doc             
139  
140  lemma cSup_lower_bounds_eq_cInf {s : set α} (h : bdd_below s) (hs : s.nonempty) :
id                                        └─┘        └───────┘         └───────┘
src                                       └─┘         └───────┘           └───────┘
typ                                       └─┘        └───────┘         └───────┘
doc                                                   └───────┘           └───────┘
141    Sup (lower_bounds s) = Inf s :=
id     └─┘  └──────────┘    └─┘ 
src    └─┘  └──────────┘     └─┘
typ    └─┘  └──────────┘    └─┘ 
doc    └─┘  └──────────┘      └─┘
142  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
143    (cSup_le h $ assume a ha, le_cInf hs ha)
id      └─────┘            └┘  └─────┘ └┘ └┘
src     └─────┘                  └─────┘
typ     └─────┘            └┘  └─────┘ └┘ └┘
144    (le_cSup (hs.mono $ λ a ha y hy, hy ha) $ assume x hx, cInf_le h hx)
id      └─────┘  └┘└───┘      └┘  └┘  └┘ └┘            └┘  └─────┘  └┘
src     └─────┘    └───┘                                      └─────┘
typ     └─────┘  └┘└───┘      └┘  └┘  └┘ └┘            └┘  └─────┘  └┘
145  
146  lemma cInf_upper_bounds_eq_cSup {s : set α} (h : bdd_above s) (hs : s.nonempty) :
id                                        └─┘        └───────┘         └───────┘
src                                       └─┘         └───────┘           └───────┘
typ                                       └─┘        └───────┘         └───────┘
doc                                                   └───────┘           └───────┘
147    Inf (upper_bounds s) = Sup s :=
id     └─┘  └──────────┘    └─┘ 
src    └─┘  └──────────┘     └─┘
typ    └─┘  └──────────┘    └─┘ 
doc    └─┘  └──────────┘      └─┘
148  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
149    (cInf_le (hs.mono $ assume a ha y hy, hy ha) $ assume x hx, le_cSup h hx)
id      └─────┘  └┘└───┘           └┘  └┘  └┘ └┘            └┘  └─────┘  └┘
src     └─────┘    └───┘                                           └─────┘
typ     └─────┘  └┘└───┘           └┘  └┘  └┘ └┘            └┘  └─────┘  └┘
150    (le_cInf h $ assume a ha, cSup_le hs ha)
id      └─────┘            └┘  └─────┘ └┘ └┘
src     └─────┘                  └─────┘
typ     └─────┘            └┘  └─────┘ └┘ └┘
151  
152  /--Introduction rule to prove that b is the supremum of s: it suffices to check that b
153  is larger than all elements of s, and that this is not the case of any w<b.-/
154  theorem cSup_intro (_ : s.nonempty) (_ : ∀a∈s, a ≤ b) (H : ∀w, w < b → (∃a∈s, w < a)) : Sup s = b :=
id                           └───────┘                                      └─┘   
src                           └───────┘                                                 └─┘   
typ                          └───────┘                                      └─┘   
doc                           └───────┘                                                      └─┘
155  have bdd_above s := ⟨b, by assumption⟩,
id        └───────┘      
src       └───────┘             └────────┘
typ       └───────┘           └────────┘
doc       └───────┘             └────────┘
txt                             └────────┘
par                             └────────┘
st                             └─────────┘
156  have (Sup s < b) ∨ (Sup s = b) := lt_or_eq_of_le (cSup_le ‹_› ‹∀a∈s, a ≤ b›),
id         └─┘       └─┘        └────────────┘  └─────┘         
src        └─┘         └─┘          └────────────┘  └─────┘             
typ        └─┘       └─┘        └────────────┘  └─────┘         
doc        └─┘           └─┘                                                
157  have ¬(Sup s < b) :=
id         └─┘   
src        └─┘   
typ        └─┘   
doc         └─┘
158    assume: Sup s < b,
id             └─┘   
src            └─┘   
typ            └─┘   
doc            └─┘
159    let ⟨a, _, _⟩ := (H (Sup s) ‹Sup s < b›) in  /- a ∈ s, Sup s < a-/
id     └─┘                └─┘   └─┘   
src                         └─┘    └─┘     
typ    └─┘                └─┘   └─┘   
doc                         └─┘    └─┘      
160    have Sup s < Sup s := lt_of_lt_of_le ‹Sup s < a› (le_cSup ‹bdd_above s› ‹a ∈ s›),
id          └─┘   └─┘     └────────────┘ └─┘      └─────┘ └───────┘     
src         └─┘    └─┘      └────────────┘ └─┘       └─────┘ └───────┘       
typ         └─┘   └─┘     └────────────┘ └─┘      └─────┘ └───────┘     
doc         └─┘     └─┘                     └─┘                └───────┘        
161    show false, by finish [lt_irrefl (Sup s)],
id          └───┘             └───────┘  └─┘ 
src         └───┘     └──────┘└───────┘ └─┘ └┘
typ         └───┘     └──────┘└───────┘ └─┘└┘
doc                   └──────┘          └─┘ └┘
txt                   └──────┘              └┘
par                   └──────┘              └┘
pid                         └┘              └┘
st                   └─────────────────────────┘
162  show Sup s = b, by finish
id        └─┘   
src       └─┘          └──────
typ       └─┘        └──────
doc       └─┘           └──────
txt                     └──────
par                     └──────
pid                           
st                     └───────
163  
src  
typ  
doc  
txt  
par  
pid  
st   
164  /--Introduction rule to prove that b is the infimum of s: it suffices to check that b
165  is smaller than all elements of s, and that this is not the case of any w>b.-/
166  theorem cInf_intro (_ : s.nonempty) (_ : ∀a∈s, b ≤ a) (H : ∀w, b < w → (∃a∈s, a < w)) : Inf s = b :=
id                           └───────┘                                      └─┘   
src                           └───────┘                                                 └─┘   
typ                          └───────┘                                      └─┘   
doc                           └───────┘                                                      └─┘
167  have bdd_below s := ⟨b, by assumption⟩,
id        └───────┘      
src       └───────┘             └────────┘
typ       └───────┘           └────────┘
doc       └───────┘             └────────┘
txt                             └────────┘
par                             └────────┘
st                             └─────────┘
168  have (b < Inf s) ∨ (b = Inf s) := lt_or_eq_of_le (le_cInf ‹_› ‹∀a∈s, b ≤ a›),
id           └─┘       └─┘      └────────────┘  └─────┘         
src           └─┘         └─┘       └────────────┘  └─────┘             
typ          └─┘       └─┘      └────────────┘  └─────┘         
doc            └─┘           └─┘                                            
169  have ¬(b < Inf s) :=
id           └─┘ 
src           └─┘
typ          └─┘ 
doc             └─┘
170    assume: b < Inf s,
id               └─┘ 
src               └─┘
typ              └─┘ 
doc                └─┘
171    let ⟨a, _, _⟩ := (H (Inf s) ‹b < Inf s›) in  /- a ∈ s, a < Inf s-/
id     └─┘                └─┘     └─┘ 
src                         └─┘       └─┘  
typ    └─┘                └─┘     └─┘ 
doc                         └─┘        └─┘  
172    have Inf s < Inf s := lt_of_le_of_lt (cInf_le ‹bdd_below s› ‹a ∈ s›) ‹a < Inf s› ,
id          └─┘   └─┘     └────────────┘  └─────┘ └───────┘          └─┘ 
src         └─┘    └─┘      └────────────┘  └─────┘ └───────┘            └─┘  
typ         └─┘   └─┘     └────────────┘  └─────┘ └───────┘          └─┘ 
doc         └─┘     └─┘                              └───────┘              └─┘  
173    show false, by finish [lt_irrefl (Inf s)],
id          └───┘             └───────┘  └─┘ 
src         └───┘     └──────┘└───────┘ └─┘ └┘
typ         └───┘     └──────┘└───────┘ └─┘└┘
doc                   └──────┘          └─┘ └┘
txt                   └──────┘              └┘
par                   └──────┘              └┘
pid                         └┘              └┘
st                   └─────────────────────────┘
174  show Inf s = b, by finish
id        └─┘   
src       └─┘          └──────
typ       └─┘        └──────
doc       └─┘           └──────
txt                     └──────
par                     └──────
pid                           
st                     └───────
175  
src  
typ  
doc  
txt  
par  
pid  
st   
176  /--When an element a of a set s is larger than all other elements of the set, it is Sup s-/
177  theorem cSup_of_mem_of_le (_ : a ∈ s) (_ : ∀w∈s, w ≤ a) : Sup s = a :=
id                                                     └─┘   
src                                                          └─┘   
typ                                                    └─┘   
doc                                                            └─┘
178  have bdd_above s := ⟨a, by assumption⟩,
id        └───────┘      
src       └───────┘             └────────┘
typ       └───────┘           └────────┘
doc       └───────┘             └────────┘
txt                             └────────┘
par                             └────────┘
st                             └─────────┘
179  have A : a ≤ Sup s := le_cSup ‹bdd_above s› ‹a ∈ s›,
id              └─┘     └─────┘ └───────┘    
src              └─┘      └─────┘ └───────┘       
typ             └─┘     └─────┘ └───────┘    
doc               └─┘              └───────┘        
180  have B : Sup s ≤ a := cSup_le ⟨a, ‹_›⟩ ‹∀w∈s, w ≤ a›,
id            └─┘       └─────┘             
src           └─┘         └─────┘                  
typ           └─┘       └─────┘             
doc           └─┘                                    
181  le_antisymm B A
id   └─────────┘  
src  └─────────┘
typ  └─────────┘  
182  
183  /--When an element a of a set s is smaller than all other elements of the set, it is Inf s-/
184  theorem cInf_of_mem_of_le (_ : a ∈ s) (_ : ∀w∈s, a ≤ w) : Inf s = a :=
id                                                     └─┘   
src                                                          └─┘   
typ                                                    └─┘   
doc                                                            └─┘
185  have bdd_below s := ⟨a, by assumption⟩,
id        └───────┘      
src       └───────┘             └────────┘
typ       └───────┘           └────────┘
doc       └───────┘             └────────┘
txt                             └────────┘
par                             └────────┘
st                             └─────────┘
186  have A : Inf s ≤ a := cInf_le ‹bdd_below s› ‹a ∈ s›,
id            └─┘       └─────┘ └───────┘    
src           └─┘         └─────┘ └───────┘       
typ           └─┘       └─────┘ └───────┘    
doc           └─┘                  └───────┘        
187  have B : a ≤ Inf s := le_cInf ⟨a, ‹_›⟩ ‹∀w∈s, a ≤ w›,
id              └─┘     └─────┘             
src              └─┘      └─────┘                  
typ             └─┘     └─────┘             
doc               └─┘                                
188  le_antisymm A B
id   └─────────┘  
src  └─────────┘
typ  └─────────┘  
189  
190  /--b < Sup s when there is an element a in s with b < a, when s is bounded above.
191  This is essentially an iff, except that the assumptions for the two implications are
192  slightly different (one needs boundedness above for one direction, nonemptiness and linear
193  order for the other one), so we formulate separately the two implications, contrary to
194  the complete_lattice case.-/
195  lemma lt_cSup_of_lt (_ : bdd_above s) (_ : a ∈ s) (_ : b < a) : b < Sup s :=
id                            └───────┘                         └─┘ 
src                           └───────┘                               └─┘
typ                           └───────┘                         └─┘ 
doc                           └───────┘                                  └─┘
196  lt_of_lt_of_le ‹b < a› (le_cSup ‹bdd_above s› ‹a ∈ s›)
id   └────────────┘     └─────┘ └───────┘    
src  └────────────┘       └─────┘ └───────┘       
typ  └────────────┘     └─────┘ └───────┘    
doc                                └───────┘        
197  
198  /--Inf s < b when there is an element a in s with a < b, when s is bounded below.
199  This is essentially an iff, except that the assumptions for the two implications are
200  slightly different (one needs boundedness below for one direction, nonemptiness and linear
201  order for the other one), so we formulate separately the two implications, contrary to
202  the complete_lattice case.-/
203  
204  lemma cInf_lt_of_lt (_ : bdd_below s) (_ : a ∈ s) (_ : a < b) : Inf s < b :=
id                            └───────┘                       └─┘   
src                           └───────┘                            └─┘   
typ                           └───────┘                       └─┘   
doc                           └───────┘                              └─┘
205  lt_of_le_of_lt (cInf_le ‹bdd_below s› ‹a ∈ s›) ‹a < b›
id   └────────────┘  └─────┘ └───────┘        
src  └────────────┘  └─────┘ └───────┘             
typ  └────────────┘  └─────┘ └───────┘        
doc                          └───────┘               
206  
207  /--The supremum of a singleton is the element of the singleton-/
208  @[simp] theorem cSup_singleton (a : α) : Sup {a} = a :=
id                                           └─┘    
src                                           └─┘    
typ                                          └─┘    
doc    └──┘                                   └─┘
209  cSup_of_mem_of_le (mem_singleton a)
id   └───────────────┘  └───────────┘ 
src  └───────────────┘  └───────────┘
typ  └───────────────┘  └───────────┘ 
doc  └───────────────┘
210    (λ b hb, set.eq_of_mem_singleton hb ▸ le_refl b)
id         └┘  └─────────────────────┘ └┘  └─────┘ 
src             └─────────────────────┘     └─────┘
typ        └┘  └─────────────────────┘ └┘  └─────┘ 
211  
212  /--The infimum of a singleton is the element of the singleton-/
213  @[simp] theorem cInf_singleton (a : α) : Inf {a} = a :=
id                                           └─┘    
src                                           └─┘    
typ                                          └─┘    
doc    └──┘                                   └─┘
214  cInf_of_mem_of_le (mem_singleton a)
id   └───────────────┘  └───────────┘ 
src  └───────────────┘  └───────────┘
typ  └───────────────┘  └───────────┘ 
doc  └───────────────┘
215    (λ b hb, set.eq_of_mem_singleton hb ▸ le_refl b)
id         └┘  └─────────────────────┘ └┘  └─────┘ 
src             └─────────────────────┘     └─────┘
typ        └┘  └─────────────────────┘ └┘  └─────┘ 
216  
217  /--If a set is bounded below and above, and nonempty, its infimum is less than or equal to
218  its supremum.-/
219  theorem cInf_le_cSup (_ : bdd_below s) (_ : bdd_above s) (_ : s.nonempty) : Inf s ≤ Sup s :=
id                             └───────┘        └───────┘        └───────┘    └─┘   └─┘ 
src                            └───────┘         └───────┘          └───────┘    └─┘    └─┘
typ                            └───────┘        └───────┘        └───────┘    └─┘   └─┘ 
doc                            └───────┘         └───────┘          └───────┘    └─┘     └─┘
220  let ⟨w, hw⟩ := ‹s.nonempty› in   /-hw : w ∈ s-/
id   └─┘           └───────┘
src                  └───────┘
typ  └─┘           └───────┘
doc                  └───────┘
221  have Inf s ≤ w := cInf_le ‹bdd_below s› ‹w ∈ s›,
id        └─┘        └─────┘ └───────┘     
src       └─┘         └─────┘ └───────┘       
typ       └─┘        └─────┘ └───────┘     
doc       └─┘                  └───────┘        
222  have w ≤ Sup s := le_cSup ‹bdd_above s› ‹w ∈ s›,
id           └─┘     └─────┘ └───────┘     
src          └─┘      └─────┘ └───────┘       
typ          └─┘     └─────┘ └───────┘     
doc           └─┘              └───────┘        
223  le_trans ‹Inf s ≤ w› ‹w ≤ Sup s›
id   └──────┘ └─┘        └─┘ 
src  └──────┘ └─┘         └─┘  
typ  └──────┘ └─┘        └─┘ 
doc           └─┘           └─┘  
224  
225  /--The sup of a union of two sets is the max of the suprema of each subset, under the assumptions
226  that all sets are bounded above and nonempty.-/
227  theorem cSup_union (_ : bdd_above s) (sne : s.nonempty) (_ : bdd_above t) (tne : t.nonempty) :
id                           └───────┘          └───────┘       └───────┘          └───────┘
src                          └───────┘            └───────┘       └───────┘            └───────┘
typ                          └───────┘          └───────┘       └───────┘          └───────┘
doc                          └───────┘            └───────┘       └───────┘            └───────┘
228  Sup (s ∪ t) = Sup s ⊔ Sup t :=
id   └─┘       └─┘   └─┘ 
src  └─┘         └─┘    └─┘
typ  └─┘       └─┘   └─┘ 
doc  └─┘           └─┘     └─┘
229  have A : Sup (s ∪ t) ≤ Sup s ⊔ Sup t :=
id            └─┘       └─┘   └─┘ 
src           └─┘         └─┘    └─┘
typ           └─┘       └─┘   └─┘ 
doc           └─┘           └─┘     └─┘
230    have (s ∪ t).nonempty := sne.inl,
id              └──────┘     └─┘└──┘
src               └──────┘        └──┘
typ             └──────┘     └─┘└──┘
doc                └──────┘
231    have F : ∀b∈ s∪t, b ≤ Sup s ⊔ Sup t :=
id                     └─┘   └─┘ 
src                        └─┘    └─┘
typ                    └─┘   └─┘ 
doc                          └─┘     └─┘
232      begin
st       └─────
233        intros,
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
st   ───────────┘└─
234        cases H,
id               
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────┘└─
235        apply le_trans (le_cSup ‹bdd_above s› ‹b ∈ s›) _, simp only [lattice.le_sup_left],
id               └──────┘  └─────┘ └───────┘                       └─────────────────┘
src        └────┘└──────┘ └─────┘└───────┘     └─┘  └─────────┘└─────────────────┘
typ        └────┘└──────┘ └─────┘└───────┘   └─┘  └─────────┘└─────────────────┘
doc        └────┘                └───────┘      └─┘  └─────────┘                   
txt        └────┘                                 └─┘  └─────────┘                   
par        └────┘                                 └─┘  └─────────┘                   
pid                                              └─┘      └──┘└┘                   
st   ─────────────────────────────────────────────────────┘└───────────────────────────────┘└─
236        apply le_trans (le_cSup ‹bdd_above t› ‹b ∈ t›) _, simp only [lattice.le_sup_right]
id               └──────┘  └─────┘  └───────┘                         └──────────────────┘
src        └────┘└──────┘ └─────┘ └───────┘       └─┘  └─────────┘└──────────────────┘└─
typ        └────┘└──────┘ └─────┘ └───────┘     └─┘  └─────────┘└──────────────────┘└─
doc        └────┘                 └───────┘       └─┘  └─────────┘                    └─
txt        └────┘                                 └─┘  └─────────┘                    └─
par        └────┘                                 └─┘  └─────────┘                    └─
pid                                              └─┘      └──┘└┘                    
st   ─────────────────────────────────────────────────────┘└──────────────────────────────────
237      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
238    cSup_le this F,
id     └─────┘ └──┘ 
src    └─────┘
typ    └─────┘ └──┘ 
239  have B : Sup s ⊔ Sup t ≤ Sup (s ∪ t) :=
id            └─┘   └─┘   └─┘    
src           └─┘    └─┘    └─┘    
typ           └─┘   └─┘   └─┘    
doc           └─┘     └─┘     └─┘
240    have Sup s ≤ Sup (s ∪ t),
id          └─┘   └─┘    
src         └─┘    └─┘    
typ         └─┘   └─┘    
doc         └─┘     └─┘
241      from cSup_le_cSup (bdd_above_union.2 ⟨‹_›, ‹_›⟩) sne (set.subset_union_left _ _),
id            └──────────┘  └─────────────┘          └─┘  └───────────────────┘
src           └──────────┘  └─────────────┘               └───────────────────┘
typ           └──────────┘  └─────────────┘          └─┘  └───────────────────┘
doc                         └─────────────┘        
242    have Sup t ≤ Sup (s ∪ t),
id          └─┘   └─┘    
src         └─┘    └─┘    
typ         └─┘   └─┘    
doc         └─┘     └─┘
243      from cSup_le_cSup (bdd_above_union.2 ⟨‹_›, ‹_›⟩) tne (set.subset_union_right _ _),
id            └──────────┘  └─────────────┘          └─┘  └────────────────────┘
src           └──────────┘  └─────────────┘               └────────────────────┘
typ           └──────────┘  └─────────────┘          └─┘  └────────────────────┘
doc                         └─────────────┘        
244    by simp only [lattice.sup_le_iff]; split; assumption,
id                   └────────────────┘
src       └─────────┘└────────────────┘  └───┘  └────────┘
typ       └─────────┘└────────────────┘  └───┘  └────────┘
doc       └─────────┘                    └───┘  └────────┘
txt       └─────────┘                    └───┘  └────────┘
par       └─────────┘                    └───┘  └────────┘
pid           └──┘└┘                  
st       └────────────────────────────────────────────────┘
245  le_antisymm A B
id   └─────────┘  
src  └─────────┘
typ  └─────────┘  
246  
247  /--The inf of a union of two sets is the min of the infima of each subset, under the assumptions
248  that all sets are bounded below and nonempty.-/
249  theorem cInf_union (_ : bdd_below s) (sne : s.nonempty) (_ : bdd_below t) (tne : t.nonempty) :
id                           └───────┘          └───────┘       └───────┘          └───────┘
src                          └───────┘            └───────┘       └───────┘            └───────┘
typ                          └───────┘          └───────┘       └───────┘          └───────┘
doc                          └───────┘            └───────┘       └───────┘            └───────┘
250  Inf (s ∪ t) = Inf s ⊓ Inf t :=
id   └─┘       └─┘   └─┘ 
src  └─┘         └─┘    └─┘
typ  └─┘       └─┘   └─┘ 
doc  └─┘           └─┘     └─┘
251  have A : Inf s ⊓ Inf t ≤ Inf (s ∪ t) :=
id            └─┘   └─┘   └─┘    
src           └─┘    └─┘    └─┘    
typ           └─┘   └─┘   └─┘    
doc           └─┘     └─┘     └─┘
252    have (s ∪ t).nonempty, from sne.inl,
id              └──────┘        └─┘└──┘
src               └──────┘           └──┘
typ             └──────┘        └─┘└──┘
doc                └──────┘
253    have F : ∀b∈ s∪t, Inf s ⊓ Inf t ≤ b :=
id                   └─┘   └─┘   
src                     └─┘    └─┘   
typ                  └─┘   └─┘   
doc                      └─┘     └─┘
254      begin
st       └─────
255        intros,
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
st   ───────────┘└─
256        cases H,
id               
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────┘└─
257        apply le_trans _ (cInf_le ‹bdd_below s› ‹b ∈ s›), simp only [lattice.inf_le_left],
id               └──────┘    └─────┘ └───────┘                     └─────────────────┘
src        └────┘└──────┘└─┘ └─────┘└───────┘       └─────────┘└─────────────────┘
typ        └────┘└──────┘└─┘ └─────┘└───────┘     └─────────┘└─────────────────┘
doc        └────┘        └─┘        └───────┘        └─────────┘                   
txt        └────┘        └─┘                           └─────────┘                   
par        └────┘        └─┘                           └─────────┘                   
pid                     └─┘                               └──┘└┘                   
st   ─────────────────────────────────────────────────────┘└───────────────────────────────┘└─
258        apply le_trans _ (cInf_le ‹bdd_below t› ‹b ∈ t›), simp only [lattice.inf_le_right]
id               └──────┘    └─────┘  └───────┘                       └──────────────────┘
src        └────┘└──────┘└─┘ └─────┘ └───────┘         └─────────┘└──────────────────┘└─
typ        └────┘└──────┘└─┘ └─────┘ └───────┘       └─────────┘└──────────────────┘└─
doc        └────┘        └─┘         └───────┘         └─────────┘                    └─
txt        └────┘        └─┘                           └─────────┘                    └─
par        └────┘        └─┘                           └─────────┘                    └─
pid                     └─┘                               └──┘└┘                    
st   ─────────────────────────────────────────────────────┘└──────────────────────────────────
259      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
260    le_cInf this F,
id     └─────┘ └──┘ 
src    └─────┘
typ    └─────┘ └──┘ 
261  have B : Inf (s ∪ t) ≤ Inf s ⊓ Inf t  :=
id            └─┘       └─┘   └─┘ 
src           └─┘         └─┘    └─┘
typ           └─┘       └─┘   └─┘ 
doc           └─┘           └─┘     └─┘
262    have Inf (s ∪ t) ≤ Inf s,
id          └─┘       └─┘ 
src         └─┘         └─┘
typ         └─┘       └─┘ 
doc         └─┘           └─┘
263      from cInf_le_cInf (bdd_below_union.2 ⟨‹_›, ‹_›⟩) sne (set.subset_union_left _ _),
id            └──────────┘  └─────────────┘          └─┘  └───────────────────┘
src           └──────────┘  └─────────────┘               └───────────────────┘
typ           └──────────┘  └─────────────┘          └─┘  └───────────────────┘
doc                         └─────────────┘        
264    have Inf (s ∪ t) ≤ Inf t,
id          └─┘       └─┘ 
src         └─┘         └─┘
typ         └─┘       └─┘ 
doc         └─┘           └─┘
265      from cInf_le_cInf (bdd_below_union.2 ⟨‹_›, ‹_›⟩) tne (set.subset_union_right _ _),
id            └──────────┘  └─────────────┘          └─┘  └────────────────────┘
src           └──────────┘  └─────────────┘               └────────────────────┘
typ           └──────────┘  └─────────────┘          └─┘  └────────────────────┘
doc                         └─────────────┘        
266    by simp only [lattice.le_inf_iff]; split; assumption; assumption,
id                   └────────────────┘
src       └─────────┘└────────────────┘  └───┘  └────────┘  └────────┘
typ       └─────────┘└────────────────┘  └───┘  └────────┘  └────────┘
doc       └─────────┘                    └───┘  └────────┘  └────────┘
txt       └─────────┘                    └───┘  └────────┘  └────────┘
par       └─────────┘                    └───┘  └────────┘  └────────┘
pid           └──┘└┘                  
st       └────────────────────────────────────────────────────────────┘
267  le_antisymm B A
id   └─────────┘  
src  └─────────┘
typ  └─────────┘  
268  
269  /--The supremum of an intersection of two sets is bounded by the minimum of the suprema of each
270  set, if all sets are bounded above and nonempty.-/
271  theorem cSup_inter_le (_ : bdd_above s) (_ : bdd_above t) (hst : (s ∩ t).nonempty) :
id                              └───────┘        └───────┘              └──────┘
src                             └───────┘         └───────┘                 └──────┘
typ                             └───────┘        └───────┘              └──────┘
doc                             └───────┘         └───────┘                  └──────┘
272  Sup (s ∩ t) ≤ Sup s ⊓ Sup t :=
id   └─┘       └─┘   └─┘ 
src  └─┘         └─┘    └─┘
typ  └─┘       └─┘   └─┘ 
doc  └─┘           └─┘     └─┘
273  begin
st   └─────
274    apply cSup_le hst, simp only [lattice.le_inf_iff, and_imp, set.mem_inter_eq], intros b _ _, split,
id           └─────┘ └─┘             └────────────────┘  └─────┘  └──────────────┘
src    └────┘└─────┘     └─────────┘└────────────────┘└┘└─────┘└┘└──────────────┘  └──────────┘  └───┘
typ    └────┘└─────┘└─┘  └─────────┘└────────────────┘└┘└─────┘└┘└──────────────┘  └──────────┘  └───┘
doc    └────┘            └─────────┘                  └┘       └┘                  └──────────┘  └───┘
txt    └────┘            └─────────┘                  └┘       └┘                  └──────────┘  └───┘
par    └────┘            └─────────┘                  └┘       └┘                  └──────────┘  └───┘
pid                         └──┘└┘                  └┘       └┘                        └────┘
st   ──────────────────┘└─────────────────────────────────────────────────────────┘└────────────┘└─────┘└─
275    apply le_cSup ‹bdd_above s› ‹b ∈ s›,
id           └─────┘ └───────┘      
src    └────┘└─────┘└───────┘   
typ    └────┘└─────┘└───────┘  
doc    └────┘       └───────┘    
txt    └────┘                      
par    └────┘                      
pid                               
st   ────────────────────────────────────┘└─
276    apply le_cSup ‹bdd_above t› ‹b ∈ t›
id           └─────┘  └───────┘        
src    └────┘└─────┘ └───────┘       
typ    └────┘└─────┘ └───────┘     
doc    └────┘        └───────┘       
txt    └────┘                        
par    └────┘                        
pid                                 
st   ─────────────────────────────────────┘
277  end
st   └─┘
278  
279  /--The infimum of an intersection of two sets is bounded below by the maximum of the
280  infima of each set, if all sets are bounded below and nonempty.-/
281  theorem le_cInf_inter (_ : bdd_below s) (_ : bdd_below t) (hst : (s ∩ t).nonempty) :
id                              └───────┘        └───────┘              └──────┘
src                             └───────┘         └───────┘                 └──────┘
typ                             └───────┘        └───────┘              └──────┘
doc                             └───────┘         └───────┘                  └──────┘
282  Inf s ⊔ Inf t ≤ Inf (s ∩ t) :=
id   └─┘   └─┘   └─┘    
src  └─┘    └─┘    └─┘    
typ  └─┘   └─┘   └─┘    
doc  └─┘     └─┘     └─┘
283  begin
st   └─────
284    apply le_cInf hst, simp only [and_imp, set.mem_inter_eq, lattice.sup_le_iff], intros b _ _, split,
id           └─────┘ └─┘             └─────┘  └──────────────┘  └────────────────┘
src    └────┘└─────┘     └─────────┘└─────┘└┘└──────────────┘└┘└────────────────┘  └──────────┘  └───┘
typ    └────┘└─────┘└─┘  └─────────┘└─────┘└┘└──────────────┘└┘└────────────────┘  └──────────┘  └───┘
doc    └────┘            └─────────┘       └┘                └┘                    └──────────┘  └───┘
txt    └────┘            └─────────┘       └┘                └┘                    └──────────┘  └───┘
par    └────┘            └─────────┘       └┘                └┘                    └──────────┘  └───┘
pid                         └──┘└┘       └┘                └┘                          └────┘
st   ──────────────────┘└─────────────────────────────────────────────────────────┘└────────────┘└─────┘└─
285    apply cInf_le ‹bdd_below s› ‹b ∈ s›,
id           └─────┘ └───────┘      
src    └────┘└─────┘└───────┘   
typ    └────┘└─────┘└───────┘  
doc    └────┘       └───────┘    
txt    └────┘                      
par    └────┘                      
pid                               
st   ────────────────────────────────────┘└─
286    apply cInf_le ‹bdd_below t› ‹b ∈ t›
id           └─────┘  └───────┘        
src    └────┘└─────┘ └───────┘       
typ    └────┘└─────┘ └───────┘     
doc    └────┘        └───────┘       
txt    └────┘                        
par    └────┘                        
pid                                 
st   ─────────────────────────────────────┘
287  end
st   └─┘
288  
289  /-- The supremum of insert a s is the maximum of a and the supremum of s, if s is
290  nonempty and bounded above.-/
291  theorem cSup_insert (_ : bdd_above s) (sne : s.nonempty) : Sup (insert a s) = a ⊔ Sup s :=
id                            └───────┘          └───────┘    └─┘  └────┘       └─┘ 
src                           └───────┘            └───────┘    └─┘  └────┘          └─┘
typ                           └───────┘          └───────┘    └─┘  └────┘       └─┘ 
doc                           └───────┘            └───────┘    └─┘                    └─┘
292  calc Sup (insert a s)
id        └─┘  └────┘  
src       └─┘  └────┘
typ       └─┘  └────┘  
doc       └─┘
293          = Sup ({a} ∪ s)   : by rw [insert_eq]
id             └─┘                  └───────┘
src            └─┘                └──┘└───────┘└─
typ            └─┘              └──┘└───────┘└─
doc            └─┘                  └──┘         └─
txt                                 └──┘         └─
par                                 └──┘         └─
pid                                   └┘         
st                                 └────────────┘
294      ... = Sup {a} ⊔ Sup s : by apply cSup_union _ _ ‹bdd_above s› sne; simp only [ne.def, not_false_iff, set.singleton_nonempty, bdd_above_singleton]
id             └─┘    └─┘             └────────┘     └───────┘  └─┘             └────┘  └───────────┘  └────────────────────┘  └─────────────────┘
src  ───┘      └─┘     └─┘        └────┘└────────┘└───┘└───────┘      └─────────┘└────┘└┘└───────────┘└┘└────────────────────┘└┘└─────────────────┘└─
typ  ───┘      └─┘    └─┘       └────┘└────────┘└───┘└───────┘└─┘  └─────────┘└────┘└┘└───────────┘└┘└────────────────────┘└┘└─────────────────┘└─
doc  ───┘      └─┘       └─┘        └────┘└────────┘└───┘└───────┘      └─────────┘      └┘             └┘                      └┘                   └─
txt  ───┘                           └────┘          └───┘                 └─────────┘      └┘             └┘                      └┘                   └─
par  ───┘                           └────┘          └───┘                 └─────────┘      └┘             └┘                      └┘                   └─
pid  ───┘                                          └───┘                     └──┘└┘      └┘             └┘                      └┘                   
st   ───┘                          └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
295      ... = a ⊔ Sup s       : by simp only [eq_self_iff_true, lattice.cSup_singleton]
id               └─┘                        └──────────────┘  └────────────────────┘
src  ───┘         └─┘              └─────────┘└──────────────┘└┘└────────────────────┘└─
typ  ───┘        └─┘             └─────────┘└──────────────┘└┘└────────────────────┘└─
doc  ───┘          └─┘              └─────────┘                └┘└────────────────────┘└─
txt  ───┘                           └─────────┘                └┘                      └─
par  ───┘                           └─────────┘                └┘                      └─
pid  ───┘                               └──┘└┘                └┘                      
st   ───┘                          └─────────────────────────────────────────────────────
296  
src  
typ  
doc  
txt  
par  
pid  
st   
297  /-- The infimum of insert a s is the minimum of a and the infimum of s, if s is
298  nonempty and bounded below.-/
299  theorem cInf_insert (_ : bdd_below s) (sne : s.nonempty) : Inf (insert a s) = a ⊓ Inf s :=
id                            └───────┘          └───────┘    └─┘  └────┘       └─┘ 
src                           └───────┘            └───────┘    └─┘  └────┘          └─┘
typ                           └───────┘          └───────┘    └─┘  └────┘       └─┘ 
doc                           └───────┘            └───────┘    └─┘                    └─┘
300  calc Inf (insert a s)
id        └─┘  └────┘  
src       └─┘  └────┘
typ       └─┘  └────┘  
doc       └─┘
301          = Inf ({a} ∪ s)   : by rw [insert_eq]
id             └─┘                  └───────┘
src            └─┘                └──┘└───────┘└─
typ            └─┘              └──┘└───────┘└─
doc            └─┘                  └──┘         └─
txt                                 └──┘         └─
par                                 └──┘         └─
pid                                   └┘         
st                                 └────────────┘
302      ... = Inf {a} ⊓ Inf s : by apply cInf_union _ _ ‹bdd_below s› sne; simp only [ne.def, not_false_iff, set.singleton_nonempty, bdd_below_singleton]
id             └─┘    └─┘             └────────┘     └───────┘  └─┘             └────┘  └───────────┘  └────────────────────┘  └─────────────────┘
src  ───┘      └─┘     └─┘        └────┘└────────┘└───┘└───────┘      └─────────┘└────┘└┘└───────────┘└┘└────────────────────┘└┘└─────────────────┘└─
typ  ───┘      └─┘    └─┘       └────┘└────────┘└───┘└───────┘└─┘  └─────────┘└────┘└┘└───────────┘└┘└────────────────────┘└┘└─────────────────┘└─
doc  ───┘      └─┘       └─┘        └────┘└────────┘└───┘└───────┘      └─────────┘      └┘             └┘                      └┘                   └─
txt  ───┘                           └────┘          └───┘                 └─────────┘      └┘             └┘                      └┘                   └─
par  ───┘                           └────┘          └───┘                 └─────────┘      └┘             └┘                      └┘                   └─
pid  ───┘                                          └───┘                     └──┘└┘      └┘             └┘                      └┘                   
st   ───┘                          └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
303      ... = a ⊓ Inf s       : by simp only [eq_self_iff_true, lattice.cInf_singleton]
id               └─┘                        └──────────────┘  └────────────────────┘
src  ───┘         └─┘              └─────────┘└──────────────┘└┘└────────────────────┘└─
typ  ───┘        └─┘             └─────────┘└──────────────┘└┘└────────────────────┘└─
doc  ───┘          └─┘              └─────────┘                └┘└────────────────────┘└─
txt  ───┘                           └─────────┘                └┘                      └─
par  ───┘                           └─────────┘                └┘                      └─
pid  ───┘                               └──┘└┘                └┘                      
st   ───┘                          └─────────────────────────────────────────────────────
304  
src  
typ  
doc  
txt  
par  
pid  
st   
305  @[simp] lemma cInf_interval : Inf {b | a ≤ b} = a :=
id                                 └─┘         
src                                └─┘           
typ                                └─┘         
doc    └──┘                        └─┘
306  cInf_of_mem_of_le (by simp only [set.mem_set_of_eq]) (λw Hw, by simp only [set.mem_set_of_eq] at Hw; apply Hw)
id   └───────────────┘                └───────────────┘      └┘                └───────────────┘
src  └───────────────┘     └─────────┘└───────────────┘             └─────────┘└───────────────┘└─────┘  └────┘
typ  └───────────────┘     └─────────┘└───────────────┘     └┘     └─────────┘└───────────────┘└─────┘  └────┘
doc  └───────────────┘     └─────────┘                              └─────────┘                 └─────┘  └────┘
txt                        └─────────┘                              └─────────┘                 └─────┘  └────┘
par                        └─────────┘                              └─────────┘                 └─────┘  └────┘
pid                            └──┘└┘                                  └──┘└┘                 └───┘       
st                        └────────────────────────────┘            └────────────────────────────────────────────┘
307  
308  @[simp] lemma cSup_interval : Sup {b | b ≤ a} = a :=
id                                 └─┘         
src                                └─┘           
typ                                └─┘         
doc    └──┘                        └─┘
309  cSup_of_mem_of_le (by simp only [set.mem_set_of_eq]) (λw Hw, by simp only [set.mem_set_of_eq] at Hw; apply Hw)
id   └───────────────┘                └───────────────┘      └┘                └───────────────┘
src  └───────────────┘     └─────────┘└───────────────┘             └─────────┘└───────────────┘└─────┘  └────┘
typ  └───────────────┘     └─────────┘└───────────────┘     └┘     └─────────┘└───────────────┘└─────┘  └────┘
doc  └───────────────┘     └─────────┘                              └─────────┘                 └─────┘  └────┘
txt                        └─────────┘                              └─────────┘                 └─────┘  └────┘
par                        └─────────┘                              └─────────┘                 └─────┘  └────┘
pid                            └──┘└┘                                  └──┘└┘                 └───┘       
st                        └────────────────────────────┘            └────────────────────────────────────────────┘
310  
311  /--The indexed supremum of two functions are comparable if the functions are pointwise comparable-/
312  lemma csupr_le_csupr {f g : ι → α} (B : bdd_above (range g)) (H : ∀x, f x ≤ g x) :
id                                         └───────┘  └───┘                
src                                          └───────┘  └───┘                  
typ                                        └───────┘  └───┘                
doc                                          └───────┘  └───┘
313    supr f ≤ supr g :=
id     └──┘   └──┘ 
src    └──┘    └──┘
typ    └──┘   └──┘ 
doc    └──┘     └──┘
314  begin
st   └─────
315    classical, by_cases hι : nonempty ι,
id                              └──────┘ 
src    └───────┘  └───────┘  └─┘└──────┘
typ    └───────┘  └───────┘  └─┘└──────┘
doc    └───────┘  └───────┘  └─┘        
txt    └───────┘  └───────┘  └─┘        
par    └───────┘  └───────┘  └─┘        
pid                         └─┘        
st   ──────────┘└────────────────────────┘└─
316    { have Rf : (range f).nonempty := range_nonempty _,
id                  └───┘               └────────────┘
src      └────────┘ └───┘ └────────────┘└────────────┘└┘
typ      └────────┘ └───┘└────────────┘└────────────┘└┘
doc      └────────┘ └───┘ └────────────┘              └┘
txt      └────────┘       └────────────┘              └┘
par      └────────┘       └────────────┘              └┘
pid      └─────┘└─┘       └───────┘└───┘              └┘
st   ───┘└──────────────────────────────────────────────┘└─
317      apply cSup_le Rf,
id             └─────┘ └┘
src      └────┘└─────┘
typ      └────┘└─────┘└┘
doc      └────┘       
txt      └────┘       
par      └────┘       
pid                  
st   ───────────────────┘└─
318      rintros y ⟨x, rfl⟩,
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid             └─────────┘
st   ─────────────────────┘└─
319      have : g x ∈ range g := ⟨x, rfl⟩,
id                  └───┘        └─┘
src      └─────┘  └───┘ └──┘  └┘└─┘
typ      └─────┘ └───┘└──┘ └┘└─┘
doc      └─────┘   └───┘ └──┘  └┘   
txt      └─────┘         └──┘  └┘   
par      └─────┘         └──┘  └┘   
pid      └───┘└┘         └──┘  └┘   
st   ───────────────────────────────────┘└─
320      exact le_cSup_of_le B this (H x) },
id             └───────────┘  └──┘   
src      └────┘└───────────┘        └┘
typ      └────┘└───────────┘└──┘ └┘
doc      └────┘                     └┘
txt      └────┘                     └┘
par      └────┘                     └┘
pid                                
st   ────────────────────────────────────┘└┘
321    { have Rf : range f = ∅, from range_eq_empty.2 hι,
id                 └───┘          └────────────┘   └┘
src      └────────┘└───┘   └───┘└────────────┘└─┘
typ      └────────┘└───┘  └───┘└────────────┘└─┘└┘
doc      └────────┘└───┘     └───┘              └─┘
txt      └────────┘          └───┘              └─┘
par      └────────┘          └───┘              └─┘
pid      └─────┘└─┘          └───┘              └─┘
st   ────────────────────────┘└────────────────────────┘└─
322      have Rg : range g = ∅, from range_eq_empty.2 hι,
id                 └───┘            └────────────┘   └┘
src      └────────┘└───┘     └───┘└────────────┘└─┘
typ      └────────┘└───┘    └───┘└────────────┘└─┘└┘
doc      └────────┘└───┘     └───┘              └─┘
txt      └────────┘          └───┘              └─┘
par      └────────┘          └───┘              └─┘
pid      └─────┘└─┘          └───┘              └─┘
st   ────────────────────────┘└────────────────────────┘└─
323      unfold supr, rw [Rf, Rg] }
id                        └┘  └┘
src      └─────────┘  └──┘  └┘  └┘
typ      └─────────┘  └──┘└┘└┘└┘└┘
doc      └─────────┘  └──┘  └┘  └┘
txt      └─────────┘  └──┘  └┘  └┘
par      └─────────┘  └──┘  └┘  └┘
pid            └───┘    └┘  └┘  
st   ──────────────┘└──────┘└──┘└─
324  end
st   ──┘
325  
326  /--The indexed supremum of a function is bounded above by a uniform bound-/
327  lemma csupr_le [nonempty ι] {f : ι → α} {c : α} (H : ∀x, f x ≤ c) : supr f ≤ c :=
id                   └──────┘                                   └──┘   
src                  └──────┘                                           └──┘   
typ                  └──────┘                                   └──┘   
doc                                                                      └──┘
328  cSup_le (range_nonempty f) (by rwa forall_range_iff)
id   └─────┘  └────────────┘           └──────────────┘
src  └─────┘  └────────────┘        └──┘└──────────────┘
typ  └─────┘  └────────────┘       └──┘└──────────────┘
doc                                 └──┘
txt                                 └──┘
par                                 └──┘
pid                                    
st                                 └───────────────────┘
329  
330  /--The indexed supremum of a function is bounded below by the value taken at one point-/
331  lemma le_csupr {f : ι → α} (H : bdd_above (range f)) {c : ι} : f c ≤ supr f :=
id                                 └───────┘  └───┘                └──┘ 
src                                  └───────┘  └───┘                    └──┘
typ                                └───────┘  └───┘                └──┘ 
doc                                  └───────┘  └───┘                     └──┘
332  le_cSup H (mem_range_self _)
id   └─────┘   └────────────┘
src  └─────┘    └────────────┘
typ  └─────┘   └────────────┘
333  
334  /--The indexed infimum of two functions are comparable if the functions are pointwise comparable-/
335  lemma cinfi_le_cinfi {f g : ι → α} (B : bdd_below (range f)) (H : ∀x, f x ≤ g x) :
id                                         └───────┘  └───┘                
src                                          └───────┘  └───┘                  
typ                                        └───────┘  └───┘                
doc                                          └───────┘  └───┘
336    infi f ≤ infi g :=
id     └──┘   └──┘ 
src    └──┘    └──┘
typ    └──┘   └──┘ 
doc    └──┘     └──┘
337  begin
st   └─────
338    classical, by_cases hι : nonempty ι,
id                              └──────┘ 
src    └───────┘  └───────┘  └─┘└──────┘
typ    └───────┘  └───────┘  └─┘└──────┘
doc    └───────┘  └───────┘  └─┘        
txt    └───────┘  └───────┘  └─┘        
par    └───────┘  └───────┘  └─┘        
pid                         └─┘        
st   ──────────┘└────────────────────────┘└─
339    { have Rg : (range g).nonempty, from range_nonempty _,
id                  └───┘                  └────────────┘
src      └────────┘ └───┘ └────────┘  └───┘└────────────┘└┘
typ      └────────┘ └───┘└────────┘  └───┘└────────────┘└┘
doc      └────────┘ └───┘ └────────┘  └───┘              └┘
txt      └────────┘       └────────┘  └───┘              └┘
par      └────────┘       └────────┘  └───┘              └┘
pid      └─────┘└─┘       └───────┘  └───┘              └┘
st   ───┘└──────────────────────────┘└─────────────────────┘└─
340      apply le_cInf Rg,
id             └─────┘ └┘
src      └────┘└─────┘
typ      └────┘└─────┘└┘
doc      └────┘       
txt      └────┘       
par      └────┘       
pid                  
st   ───────────────────┘└─
341      rintros y ⟨x, rfl⟩,
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid             └─────────┘
st   ─────────────────────┘└─
342      have : f x ∈ range f := ⟨x, rfl⟩,
id                  └───┘        └─┘
src      └─────┘  └───┘ └──┘  └┘└─┘
typ      └─────┘ └───┘└──┘ └┘└─┘
doc      └─────┘   └───┘ └──┘  └┘   
txt      └─────┘         └──┘  └┘   
par      └─────┘         └──┘  └┘   
pid      └───┘└┘         └──┘  └┘   
st   ───────────────────────────────────┘└─
343      exact cInf_le_of_le B this (H x) },
id             └───────────┘  └──┘   
src      └────┘└───────────┘        └┘
typ      └────┘└───────────┘└──┘ └┘
doc      └────┘                     └┘
txt      └────┘                     └┘
par      └────┘                     └┘
pid                                
st   ────────────────────────────────────┘└┘
344    { have Rf : range f = ∅, from range_eq_empty.2 hι,
id                 └───┘          └────────────┘   └┘
src      └────────┘└───┘   └───┘└────────────┘└─┘
typ      └────────┘└───┘  └───┘└────────────┘└─┘└┘
doc      └────────┘└───┘     └───┘              └─┘
txt      └────────┘          └───┘              └─┘
par      └────────┘          └───┘              └─┘
pid      └─────┘└─┘          └───┘              └─┘
st   ────────────────────────┘└────────────────────────┘└─
345      have Rg : range g = ∅, from range_eq_empty.2 hι,
id                 └───┘            └────────────┘   └┘
src      └────────┘└───┘     └───┘└────────────┘└─┘
typ      └────────┘└───┘    └───┘└────────────┘└─┘└┘
doc      └────────┘└───┘     └───┘              └─┘
txt      └────────┘          └───┘              └─┘
par      └────────┘          └───┘              └─┘
pid      └─────┘└─┘          └───┘              └─┘
st   ────────────────────────┘└────────────────────────┘└─
346      unfold infi, rw [Rf, Rg] }
id                        └┘  └┘
src      └─────────┘  └──┘  └┘  └┘
typ      └─────────┘  └──┘└┘└┘└┘└┘
doc      └─────────┘  └──┘  └┘  └┘
txt      └─────────┘  └──┘  └┘  └┘
par      └─────────┘  └──┘  └┘  └┘
pid            └───┘    └┘  └┘  
st   ──────────────┘└──────┘└──┘└─
347  end
st   ──┘
348  
349  /--The indexed minimum of a function is bounded below by a uniform lower bound-/
350  lemma le_cinfi [nonempty ι] {f : ι → α} {c : α} (H : ∀x, c ≤ f x) : c ≤ infi f :=
id                   └──────┘                                     └──┘ 
src                  └──────┘                                              └──┘
typ                  └──────┘                                     └──┘ 
doc                                                                          └──┘
351  le_cInf (range_nonempty f) (by rwa forall_range_iff)
id   └─────┘  └────────────┘           └──────────────┘
src  └─────┘  └────────────┘        └──┘└──────────────┘
typ  └─────┘  └────────────┘       └──┘└──────────────┘
doc                                 └──┘
txt                                 └──┘
par                                 └──┘
pid                                    
st                                 └───────────────────┘
352  
353  /--The indexed infimum of a function is bounded above by the value taken at one point-/
354  lemma cinfi_le {f : ι → α} (H : bdd_below (range f)) {c : ι} : infi f ≤ f c :=
id                                 └───────┘  └───┘             └──┘    
src                                  └───────┘  └───┘               └──┘   
typ                                └───────┘  └───┘             └──┘    
doc                                  └───────┘  └───┘               └──┘
355  cInf_le H (mem_range_self _)
id   └─────┘   └────────────┘
src  └─────┘    └────────────┘
typ  └─────┘   └────────────┘
356  
357  lemma is_lub_cSup {s : set α} (ne : s.nonempty) (H : bdd_above s) : is_lub s (Sup s) :=
id                          └─┘         └───────┘       └───────┘     └────┘   └─┘ 
src                         └─┘           └───────┘       └───────┘      └────┘    └─┘
typ                         └─┘         └───────┘       └───────┘     └────┘   └─┘ 
doc                                       └───────┘       └───────┘      └────┘    └─┘
358  ⟨assume x, le_cSup H, assume x, cSup_le ne⟩
id             └─────┘            └─────┘ └┘
src             └─────┘              └─────┘ └┘
typ            └─────┘            └─────┘ └┘
359  
360  lemma is_glb_cInf {s : set α} (ne : s.nonempty) (H : bdd_below s) : is_glb s (Inf s) :=
id                          └─┘         └───────┘       └───────┘     └────┘   └─┘ 
src                         └─┘           └───────┘       └───────┘      └────┘    └─┘
typ                         └─┘         └───────┘       └───────┘     └────┘   └─┘ 
doc                                       └───────┘       └───────┘      └────┘    └─┘
361  ⟨assume x, cInf_le H, assume x, le_cInf ne⟩
id             └─────┘            └─────┘ └┘
src             └─────┘              └─────┘ └┘
typ            └─────┘            └─────┘ └┘
362  
363  @[simp] theorem cinfi_const [hι : nonempty ι] {a : α} : (⨅ b:ι, a) = a :=
id                                     └──────┘                    
src                                    └──────┘                       
typ                                    └──────┘                    
doc    └──┘                                                       
364  begin
st   └─────
365    refine hι.elim (λ x, _),
id            └─────┘
src    └─────┘└─────┘  └────┘
typ    └─────┘└─────┘  └────┘
doc    └─────┘         └────┘
txt    └─────┘         └────┘
par    └─────┘         └────┘
pid                   └────┘
st   ────────────────────────┘└─
366    refine le_antisymm (@cinfi_le _ _ _ _ _ x) (le_cinfi (λi, _root_.le_refl _)),
id            └─────────┘   └──────┘              └──────┘      └────────────┘
src    └─────┘└─────────┘  └──────┘└─────────┘ └┘ └──────┘  └─┘└────────────┘└──┘
typ    └─────┘└─────────┘  └──────┘└─────────┘└┘ └──────┘  └─┘└────────────┘└──┘
doc    └─────┘             └──────┘└─────────┘ └┘ └──────┘  └─┘              └──┘
txt    └─────┘                     └─────────┘ └┘           └─┘              └──┘
par    └─────┘                     └─────────┘ └┘           └─┘              └──┘
pid                               └─────────┘ └┘           └─┘              └──┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
367    rw range_const,
id        └─────────┘
src    └─┘└─────────┘
typ    └─┘└─────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────┘└─
368    exact bdd_below_singleton
id           └─────────────────┘
src    └────┘└─────────────────┘
typ    └────┘└─────────────────┘
doc    └────┘                   
txt    └────┘                   
par    └────┘                   
pid                            
st   ───────────────────────────┘
369  end
st   └─┘
370  
371  @[simp] theorem csupr_const [hι : nonempty ι] {a : α} : (⨆ b:ι, a) = a :=
id                                     └──────┘                    
src                                    └──────┘                       
typ                                    └──────┘                    
doc    └──┘                                                       
372  begin
st   └─────
373    refine hι.elim (λ x, _),
id            └─────┘
src    └─────┘└─────┘  └────┘
typ    └─────┘└─────┘  └────┘
doc    └─────┘         └────┘
txt    └─────┘         └────┘
par    └─────┘         └────┘
pid                   └────┘
st   ────────────────────────┘└─
374    refine le_antisymm (csupr_le (λi, _root_.le_refl _)) (@le_csupr _ _ _ (λ b:ι, a) _ x),
id            └─────────┘  └──────┘      └────────────┘       └──────┘                  
src    └─────┘└─────────┘ └──────┘  └─┘└────────────┘└───┘  └──────┘└─────┘  └─┘ └┘ └──┘ 
typ    └─────┘└─────────┘ └──────┘  └─┘└────────────┘└───┘  └──────┘└─────┘  └─┘└┘└──┘
doc    └─────┘            └──────┘  └─┘              └───┘  └──────┘└─────┘  └─┘ └┘ └──┘ 
txt    └─────┘                      └─┘              └───┘          └─────┘  └─┘ └┘ └──┘ 
par    └─────┘                      └─┘              └───┘          └─────┘  └─┘ └┘ └──┘ 
pid                                └─┘              └───┘          └─────┘  └─┘ └┘ └──┘ 
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
375    rw range_const,
id        └─────────┘
src    └─┘└─────────┘
typ    └─┘└─────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────┘└─
376    exact bdd_above_singleton
id           └─────────────────┘
src    └────┘└─────────────────┘
typ    └────┘└─────────────────┘
doc    └────┘                   
txt    └────┘                   
par    └────┘                   
pid                            
st   ───────────────────────────┘
377  end
st   └─┘
378  
379  end conditionally_complete_lattice
380  
381  
382  section conditionally_complete_linear_order
383  variables [conditionally_complete_linear_order α] {s t : set α} {a b : α}
id              └─────────────────────────────────┘           └─┘
src             └─────────────────────────────────┘           └─┘
typ             └─────────────────────────────────┘           └─┘
384  
385  /-- When b < Sup s, there is an element a in s with b < a, if s is nonempty and the order is
386  a linear order. -/
387  lemma exists_lt_of_lt_cSup (hs : s.nonempty) (hb : b < Sup s) : ∃a∈s, b < a :=
id                                    └───────┘          └─┘         
src                                    └───────┘           └─┘            
typ                                   └───────┘          └─┘         
doc                                    └───────┘            └─┘
388  begin
st   └─────
389    classical, contrapose! hb,
src    └───────┘  └────────────┘
typ    └───────┘  └────────────┘
doc    └───────┘  └────────────┘
txt    └───────┘  └────────────┘
par    └───────┘  └────────────┘
pid                         └─┘
st   ──────────┘└──────────────┘└─
390    exact cSup_le hs hb
id           └─────┘ └┘ └┘
src    └────┘└─────┘    
typ    └────┘└─────┘└┘└┘
doc    └────┘           
txt    └────┘           
par    └────┘           
pid                    
st   ─────────────────────┘
391  end
st   └─┘
392  
393  /--
394  Indexed version of the above lemma `exists_lt_of_lt_cSup`.
395  When `b < supr f`, there is an element `i` such that `b < f i`.
396  -/
397  lemma exists_lt_of_lt_csupr [nonempty ι] {f : ι → α} (h : b < supr f) :
id                                └──────┘                    └──┘ 
src                               └──────┘                        └──┘
typ                               └──────┘                    └──┘ 
doc                                                                └──┘
398    ∃i, b < f i :=
id         
src        
typ        
399  let ⟨_, ⟨i, rfl⟩, h⟩ := exists_lt_of_lt_cSup (range_nonempty f) h in ⟨i, h⟩
id   └─┘        └─┘        └──────────────────┘  └────────────┘   
src              └─┘         └──────────────────┘  └────────────┘
typ  └─┘        └─┘        └──────────────────┘  └────────────┘   
doc                          └──────────────────┘
400  
401  /--When Inf s < b, there is an element a in s with a < b, if s is nonempty and the order is
402  a linear order.-/
403  lemma exists_lt_of_cInf_lt (hs : s.nonempty) (hb : Inf s < b) : ∃a∈s, a < b :=
id                                    └───────┘        └─┘           
src                                    └───────┘        └─┘               
typ                                   └───────┘        └─┘           
doc                                    └───────┘        └─┘
404  begin
st   └─────
405    classical, contrapose! hb,
src    └───────┘  └────────────┘
typ    └───────┘  └────────────┘
doc    └───────┘  └────────────┘
txt    └───────┘  └────────────┘
par    └───────┘  └────────────┘
pid                         └─┘
st   ──────────┘└──────────────┘└─
406    exact le_cInf hs hb
id           └─────┘ └┘ └┘
src    └────┘└─────┘    
typ    └────┘└─────┘└┘└┘
doc    └────┘           
txt    └────┘           
par    └────┘           
pid                    
st   ─────────────────────┘
407  end
st   └─┘
408  
409  /--
410  Indexed version of the above lemma `exists_lt_of_cInf_lt`
411  When `infi f < a`, there is an element `i` such that `f i < a`.
412  -/
413  lemma exists_lt_of_cinfi_lt [nonempty ι] {f : ι → α} (h : infi f < a) :
id                                └──────┘                  └──┘   
src                               └──────┘                     └──┘   
typ                               └──────┘                  └──┘   
doc                                                            └──┘
414    (∃i, f i < a) :=
id          
src           
typ         
415  let ⟨_, ⟨i, rfl⟩, h⟩ := exists_lt_of_cInf_lt (range_nonempty f) h in ⟨i, h⟩
id   └─┘        └─┘        └──────────────────┘  └────────────┘   
src              └─┘         └──────────────────┘  └────────────┘
typ  └─┘        └─┘        └──────────────────┘  └────────────┘   
doc                          └──────────────────┘
416  
417  /--Introduction rule to prove that b is the supremum of s: it suffices to check that
418  1) b is an upper bound
419  2) every other upper bound b' satisfies b ≤ b'.-/
420  theorem cSup_intro' (_ : s.nonempty)
id                            └───────┘
src                            └───────┘
typ                           └───────┘
doc                            └───────┘
421    (h_is_ub : ∀ a ∈ s, a ≤ b) (h_b_le_ub : ∀ub, (∀ a ∈ s, a ≤ ub) → (b ≤ ub)) : Sup s = b :=
id                                         └┘            └┘       └┘     └─┘   
src                                                                              └─┘   
typ                                        └┘            └┘       └┘     └─┘   
doc                                                                                 └─┘
422  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
423    (show Sup s ≤ b, from cSup_le ‹s.nonempty› h_is_ub)
id           └─┘          └─────┘ └───────┘ └─────┘
src          └─┘            └─────┘  └───────┘
typ          └─┘          └─────┘ └───────┘ └─────┘
doc          └─┘                      └───────┘
424    (show b ≤ Sup s, from h_b_le_ub _ $ assume a, le_cSup ⟨b, h_is_ub⟩)
id             └─┘        └───────┘              └─────┘    └─────┘
src             └─┘                                 └─────┘
typ            └─┘        └───────┘              └─────┘    └─────┘
doc              └─┘
425  
426  end conditionally_complete_linear_order
427  
428  section conditionally_complete_linear_order_bot
429  
430  lemma cSup_empty [conditionally_complete_linear_order_bot α] : (Sup ∅ : α) = ⊥ :=
id                     └─────────────────────────────────────┘      └─┘       
src                    └─────────────────────────────────────┘       └─┘        
typ                    └─────────────────────────────────────┘      └─┘       
doc                                                                  └─┘
431  conditionally_complete_linear_order_bot.cSup_empty α
id   └────────────────────────────────────────────────┘ 
src  └────────────────────────────────────────────────┘
typ  └────────────────────────────────────────────────┘ 
432  
433  end conditionally_complete_linear_order_bot
434  
435  section
436  
437  open_locale classical
438  
439  noncomputable instance : has_Inf ℕ :=
id                            └─────┘ 
src                           └─────┘ 
typ                           └─────┘ 
doc                           └─────┘
440  ⟨λs, if h : ∃n, n ∈ s then @nat.find (λn, n ∈ s) _ h else 0⟩
id       └┘               └──────┘                 
src       └┘                  └──────┘                     
typ      └┘               └──────┘                 
441  
442  noncomputable instance : has_Sup ℕ :=
id                            └─────┘ 
src                           └─────┘ 
typ                           └─────┘ 
doc                           └─────┘
443  ⟨λs, if h : ∃n, ∀a∈s, a ≤ n then @nat.find (λn, ∀a∈s, a ≤ n) _ h else 0⟩
id       └┘                   └──────┘                     
src       └┘                        └──────┘              
typ      └┘                   └──────┘                     
444  
445  lemma Inf_nat_def {s : set ℕ} (h : ∃n, n ∈ s) : Inf s = @nat.find (λn, n ∈ s) _ h :=
id                          └─┘               └─┘    └──────┘           
src                         └─┘                  └─┘     └──────┘        
typ                         └─┘               └─┘    └──────┘           
doc                                                  └─┘
446  dif_pos _
id   └─────┘
src  └─────┘
typ  └─────┘
447  
448  lemma Sup_nat_def {s : set ℕ} (h : ∃n, ∀a∈s, a ≤ n) :
id                          └─┘               
src                         └─┘                  
typ                         └─┘               
449    Sup s = @nat.find (λn, ∀a∈s, a ≤ n) _ h :=
id     └─┘    └──────┘               
src    └─┘     └──────┘              
typ    └─┘    └──────┘               
doc    └─┘
450  dif_pos _
id   └─────┘
src  └─────┘
typ  └─────┘
451  
452  /-- This instance is necessary, otherwise the lattice operations would be derived via
453  conditionally_complete_linear_order_bot and marked as noncomputable. -/
454  instance : lattice ℕ := infer_instance
id              └─────┘     └────────────┘
src             └─────┘     └────────────┘
typ             └─────┘     └────────────┘
doc             └─────┘      └────────────┘
455  
456  noncomputable instance : conditionally_complete_linear_order_bot ℕ :=
id                            └─────────────────────────────────────┘ 
src                           └─────────────────────────────────────┘ 
typ                           └─────────────────────────────────────┘ 
457  { Sup := Sup, Inf := Inf,
id            └─┘         └─┘
src           └─┘         └─┘
typ           └─┘         └─┘
doc           └─┘         └─┘
458    le_cSup    := assume s a hb ha, by rw [Sup_nat_def hb]; revert a ha; exact @nat.find_spec _ _ hb,
id                            └┘ └┘         └─────────┘ └┘                       └───────────┘     └┘
src                                       └──┘└─────────┘    └─────────┘  └────┘ └───────────┘└───┘
typ                           └┘ └┘     └──┘└─────────┘└┘  └─────────┘  └────┘ └───────────┘└───┘└┘
doc                                       └──┘               └─────────┘  └────┘              └───┘
txt                                       └──┘               └─────────┘  └────┘              └───┘
par                                       └──┘               └─────────┘  └────┘              └───┘
pid                                         └┘                     └───┘                     └───┘
st                                       └─────────────────┘└────────────────────────────────────────┘
459    cSup_le    := assume s a hs ha, by rw [Sup_nat_def ⟨a, ha⟩]; exact nat.find_min' _ ha,
id                            └┘ └┘         └─────────┘    └┘          └───────────┘   └┘
src                                       └──┘└─────────┘  └┘  └┘  └────┘└───────────┘└─┘
typ                           └┘ └┘     └──┘└─────────┘ └┘└┘└┘  └────┘└───────────┘└─┘└┘
doc                                       └──┘             └┘  └┘  └────┘             └─┘
txt                                       └──┘             └┘  └┘  └────┘             └─┘
par                                       └──┘             └┘  └┘  └────┘             └─┘
pid                                         └┘             └┘  └┘                    └─┘
st                                       └──────────────────────┘└────────────────────────┘
460    le_cInf    := assume s a hs hb,
id                            └┘ └┘
typ                           └┘ └┘
461      by rw [Inf_nat_def hs]; exact hb (@nat.find_spec (λn, n ∈ s) _ _),
id              └─────────┘ └┘         └┘   └───────────┘         
src         └──┘└─────────┘    └────┘    └───────────┘  └─┘  └────┘
typ         └──┘└─────────┘└┘  └────┘└┘  └───────────┘  └─┘ └────┘
doc         └──┘               └────┘                   └─┘   └────┘
txt         └──┘               └────┘                   └─┘   └────┘
par         └──┘               └────┘                   └─┘   └────┘
pid           └┘                                       └─┘   └────┘
st         └─────────────────┘└─────────────────────────────────────────┘
462    cInf_le    := assume s a hb ha, by rw [Inf_nat_def ⟨a, ha⟩]; exact nat.find_min' _ ha,
id                            └┘ └┘         └─────────┘    └┘          └───────────┘   └┘
src                                       └──┘└─────────┘  └┘  └┘  └────┘└───────────┘└─┘
typ                           └┘ └┘     └──┘└─────────┘ └┘└┘└┘  └────┘└───────────┘└─┘└┘
doc                                       └──┘             └┘  └┘  └────┘             └─┘
txt                                       └──┘             └┘  └┘  └────┘             └─┘
par                                       └──┘             └┘  └┘  └────┘             └─┘
pid                                         └┘             └┘  └┘                    └─┘
st                                       └──────────────────────┘└────────────────────────┘
463    cSup_empty :=
464    begin
st     └─────
465      simp only [Sup_nat_def, set.mem_empty_eq, forall_const, forall_prop_of_false, not_false_iff, exists_const],
id                  └─────────┘  └──────────────┘  └──────────┘  └──────────────────┘  └───────────┘  └──────────┘
src      └─────────┘└─────────┘└┘└──────────────┘└┘└──────────┘└┘└──────────────────┘└┘└───────────┘└┘└──────────┘
typ      └─────────┘└─────────┘└┘└──────────────┘└┘└──────────┘└┘└──────────────────┘└┘└───────────┘└┘└──────────┘
doc      └─────────┘           └┘                └┘            └┘                    └┘             └┘            
txt      └─────────┘           └┘                └┘            └┘                    └┘             └┘            
par      └─────────┘           └┘                └┘            └┘                    └┘             └┘            
pid          └──┘└┘           └┘                └┘            └┘                    └┘             └┘            
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
466      apply bot_unique (nat.find_min' _ _),
id             └────────┘  └───────────┘
src      └────┘└────────┘ └───────────┘└───┘
typ      └────┘└────────┘ └───────────┘└───┘
doc      └────┘                        └───┘
txt      └────┘                        └───┘
par      └────┘                        └───┘
pid                                   └───┘
st   ───────────────────────────────────────┘└─
467      trivial
src      └───────
typ      └───────
doc      └───────
txt      └───────
par      └───────
pid             
st   ────────────
468    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
469    .. (infer_instance : order_bot ℕ), .. (infer_instance : lattice ℕ),
id         └────────────┘   └───────┘        └────────────┘   └─────┘ 
src        └────────────┘   └───────┘        └────────────┘   └─────┘ 
typ        └────────────┘   └───────┘        └────────────┘   └─────┘ 
doc        └────────────┘   └───────┘         └────────────┘   └─────┘
470    .. (infer_instance : decidable_linear_order ℕ) }
id         └────────────┘   └────────────────────┘ 
src        └────────────┘   └────────────────────┘ 
typ        └────────────┘   └────────────────────┘ 
doc        └────────────┘
471  
472  end
473  
474  end lattice /-end of namespace lattice-/
475  
476  namespace with_top
477  open lattice
478  open_locale classical
479  
480  variables [conditionally_complete_linear_order_bot α]
id              └─────────────────────────────────────┘
src             └─────────────────────────────────────┘
typ             └─────────────────────────────────────┘
481  
482  /-- The Sup of a non-empty set is its least upper bound for a conditionally
483  complete lattice with a top. -/
484  lemma is_lub_Sup' {β : Type*} [conditionally_complete_lattice β]
id                                  └────────────────────────────┘ 
src                                 └────────────────────────────┘
typ                                 └────────────────────────────┘ 
doc                                 └────────────────────────────┘
485    {s : set (with_top β)} (hs : s.nonempty) : is_lub s (Sup s) :=
id          └─┘  └──────┘          └───────┘    └────┘   └─┘ 
src         └─┘  └──────┘            └───────┘    └────┘    └─┘
typ         └─┘  └──────┘          └───────┘    └────┘   └─┘ 
doc                                  └───────┘    └────┘    └─┘
486  begin
st   └─────
487    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
488    { show ite _ _ _ ∈ _,
id            └─┘       
src      └───┘└─┘└─────┘└┘
typ      └───┘└─┘└─────┘└┘
doc      └───┘   └─────┘ └┘
txt      └───┘   └─────┘ └┘
par      └───┘   └─────┘ └┘
pid      └───┘   └─────┘ └┘
st   ───┘└────────────────┘└─
489      split_ifs,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
st   ────────────┘└─
490      { intros _ _, exact le_top },
id                           └────┘
src        └────────┘  └────┘└────┘
typ        └────────┘  └────┘└────┘
doc        └────────┘  └────┘      
txt        └────────┘  └────┘      
par        └────────┘  └────┘      
pid              └──┘             
st   ─────┘└────────┘└─────────────┘└┘
491      { rintro (⟨⟩|a) ha,
src        └──────────────┘
typ        └──────────────┘
doc        └──────────────┘
txt        └──────────────┘
par        └──────────────┘
pid              └────────┘
st   ─────┘└──────────────┘└─
492        { contradiction },
src          └────────────┘
typ          └────────────┘
doc          └────────────┘
txt          └────────────┘
par          └────────────┘
pid                       
st   ───────┘└────────────┘└┘
493        apply some_le_some.2,
id               └──────────┘
src        └────┘└──────────┘└┘
typ        └────┘└──────────┘└┘
doc        └────┘            └┘
txt        └────┘            └┘
par        └────┘            └┘
pid                         └┘
st   ─────────────────────────┘└─
494        exact le_cSup h_1 ha },
id               └─────┘ └─┘ └┘
src        └────┘└─────┘     
typ        └────┘└─────┘└─┘└┘
doc        └────┘            
txt        └────┘            
par        └────┘            
pid                         
st   ──────────────────────────┘└┘
495      { intros _ _, exact le_top } },
id                           └────┘
src        └────────┘  └────┘└────┘
typ        └────────┘  └────┘└────┘
doc        └────────┘  └────┘      
txt        └────────┘  └────┘      
par        └────────┘  └────┘      
pid              └──┘             
st   ───────────────┘└─────────────┘└──┘
496    { show ite _ _ _ ∈ _,
id            └─┘
src      └───┘└─┘└─────┘ └┘
typ      └───┘└─┘└─────┘ └┘
doc      └───┘   └─────┘ └┘
txt      └───┘   └─────┘ └┘
par      └───┘   └─────┘ └┘
pid      └───┘   └─────┘ └┘
st   ─────────────────────┘└─
497      split_ifs,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
st   ────────────┘└─
498      { rintro (⟨⟩|a) ha,
src        └──────────────┘
typ        └──────────────┘
doc        └──────────────┘
txt        └──────────────┘
par        └──────────────┘
pid              └────────┘
st   ─────┘└──────────────┘└─
499        { exact _root_.le_refl _ },
id                 └────────────┘
src          └────┘└────────────┘└─┘
typ          └────┘└────────────┘└─┘
doc          └────┘              └─┘
txt          └────┘              └─┘
par          └────┘              └─┘
pid                             └┘
st   ───────┘└─────────────────────┘└┘
500        { exact false.elim (not_top_le_coe a (ha h)) } },
id                 └────────┘  └────────────┘   └┘ 
src          └────┘└────────┘ └────────────┘     └─┘
typ          └────┘└────────┘ └────────────┘ └┘└─┘
doc          └────┘                              └─┘
txt          └────┘                              └─┘
par          └────┘                              └─┘
pid                                             └┘
st   ──────────────────────────────────────────────────┘└──┘
501      { rintro (⟨⟩|b) hb,
src        └──────────────┘
typ        └──────────────┘
doc        └──────────────┘
txt        └──────────────┘
par        └──────────────┘
pid              └────────┘
st   ─────┘└──────────────┘└─
502        { exact le_top },
id                 └────┘
src          └────┘└────┘
typ          └────┘└────┘
doc          └────┘      
txt          └────┘      
par          └────┘      
pid                     
st   ───────┘└───────────┘└┘
503        refine some_le_some.2 (cSup_le _ _),
id                └──────────┘    └─────┘
src        └─────┘└──────────┘└─┘ └─────┘└───┘
typ        └─────┘└──────────┘└─┘ └─────┘└───┘
doc        └─────┘            └─┘        └───┘
txt        └─────┘            └─┘        └───┘
par        └─────┘            └─┘        └───┘
pid                          └─┘        └───┘
st   ────────────────────────────────────────┘└─
504        { rcases hs with ⟨⟨⟩|b, hb⟩,
id                  └┘
src          └─────┘  └──────────────┘
typ          └─────┘└┘└──────────────┘
doc          └─────┘  └──────────────┘
txt          └─────┘  └──────────────┘
par          └─────┘  └──────────────┘
pid                  └──────────────┘
st   ───────┘└───────────────────────┘└─
505          { exact absurd hb h },
id                   └────┘ └┘ 
src            └────┘└────┘   
typ            └────┘└────┘└┘
doc            └────┘         
txt            └────┘         
par            └────┘         
pid                          
st   ─────────┘└────────────────┘└┘
506          { exact ⟨b, hb⟩ } },
id                      └┘
src            └────┘  └┘  └┘
typ            └────┘ └┘└┘└┘
doc            └────┘  └┘  └┘
txt            └────┘  └┘  └┘
par            └────┘  └┘  └┘
pid                   └┘  
st   ───────────────────────┘└──┘
507        { intros a ha, exact some_le_some.1 (hb ha) } },
id                              └──────────┘    └┘ └┘
src          └─────────┘  └────┘└──────────┘└─┘     └┘
typ          └─────────┘  └────┘└──────────┘└─┘ └┘└┘└┘
doc          └─────────┘  └────┘            └─┘     └┘
txt          └─────────┘  └────┘            └─┘     └┘
par          └─────────┘  └────┘            └─┘     └┘
pid                └───┘                   └─┘     
st   ──────────────────┘└─────────────────────────────┘└──┘
508      { rintro (⟨⟩|b) hb,
src        └──────────────┘
typ        └──────────────┘
doc        └──────────────┘
txt        └──────────────┘
par        └──────────────┘
pid              └────────┘
st   ─────────────────────┘└─
509        { exact _root_.le_refl _ },
id                 └────────────┘
src          └────┘└────────────┘└─┘
typ          └────┘└────────────┘└─┘
doc          └────┘              └─┘
txt          └────┘              └─┘
par          └────┘              └─┘
pid                             └┘
st   ───────┘└─────────────────────┘└┘
510        { exfalso, apply h_1, use b, intros a ha, exact some_le_some.1 (hb ha) } } }
id                                                        └──────────┘    └┘ └┘
src          └─────┘  └────┘     └──┘   └─────────┘  └────┘└──────────┘└─┘     └┘
typ          └─────┘  └────┘     └──┘  └─────────┘  └────┘└──────────┘└─┘ └┘└┘└┘
doc          └─────┘  └────┘     └──┘   └─────────┘  └────┘            └─┘     └┘
txt          └─────┘  └────┘     └──┘   └─────────┘  └────┘            └─┘     └┘
par          └─────┘  └────┘     └──┘   └─────────┘  └────┘            └─┘     └┘
pid                                         └───┘                   └─┘     
st   ──────────────┘└─────────┘└─────┘└───────────┘└─────────────────────────────┘└─────
511  end
st   ──┘
512  
513  lemma is_lub_Sup (s : set (with_top α)) : is_lub s (Sup s) :=
id                         └─┘  └──────┘      └────┘   └─┘ 
src                        └─┘  └──────┘       └────┘    └─┘
typ                        └─┘  └──────┘      └────┘   └─┘ 
doc                                            └────┘    └─┘
514  begin
st   └─────
515    cases s.eq_empty_or_nonempty with hs hs,
id           └────────────────────┘
src    └────┘└────────────────────┘└─────────┘
typ    └────┘└────────────────────┘└─────────┘
doc    └────┘                      └─────────┘
txt    └────┘                      └─────────┘
par    └────┘                      └─────────┘
pid                               └─────────┘
st   ────────────────────────────────────────┘└─
516    { rw hs,
id          └┘
src      └─┘
typ      └─┘└┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└───┘└─
517      show is_lub ∅ (ite _ _ _),
id            └────┘   └─┘
src      └───┘└────┘ └─┘└─────┘
typ      └───┘└────┘ └─┘└─────┘
doc      └───┘└────┘     └─────┘
txt      └───┘           └─────┘
par      └───┘           └─────┘
pid      └───┘           └─────┘
st   ────────────────────────────┘└─
518      split_ifs,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
st   ────────────┘└─
519      { cases h },
id               
src        └────┘ 
typ        └────┘
doc        └────┘ 
txt        └────┘ 
par        └────┘ 
pid              
st   ─────┘└──────┘└┘
520      { rw [preimage_empty, cSup_empty], exact is_lub_empty },
id             └────────────┘  └────────┘         └──────────┘
src        └──┘└────────────┘└┘└────────┘  └────┘└──────────┘
typ        └──┘└────────────┘└┘└────────┘  └────┘└──────────┘
doc        └──┘              └┘            └────┘            
txt        └──┘              └┘            └────┘            
par        └──┘              └┘            └────┘            
pid          └┘              └┘                             
st   ─────┘└────────────────┘└──────────┘└────────────────────┘└┘
521      { exfalso, apply h_1, use ⊥, rintro a ⟨⟩ } },
id                                 
src        └─────┘  └────┘     └──┘  └──────────┘
typ        └─────┘  └────┘     └──┘  └──────────┘
doc        └─────┘  └────┘     └──┘   └──────────┘
txt        └─────┘  └────┘     └──┘   └──────────┘
par        └─────┘  └────┘     └──┘   └──────────┘
pid                                       └───┘
st   ────────────┘└─────────┘└─────┘└────────────┘└──┘
522    exact is_lub_Sup' hs,
id           └─────────┘ └┘
src    └────┘└─────────┘
typ    └────┘└─────────┘└┘
doc    └────┘└─────────┘
txt    └────┘           
par    └────┘           
pid                    
st   ─────────────────────┘└─
523  end
st   ──┘
524  
525  /-- The Inf of a bounded-below set is its greatest lower bound for a conditionally
526  complete lattice with a top. -/
527  lemma is_glb_Inf' {β : Type*} [conditionally_complete_lattice β]
id                                  └────────────────────────────┘ 
src                                 └────────────────────────────┘
typ                                 └────────────────────────────┘ 
doc                                 └────────────────────────────┘
528    {s : set (with_top β)} (hs : bdd_below s) : is_glb s (Inf s) :=
id          └─┘  └──────┘          └───────┘     └────┘   └─┘ 
src         └─┘  └──────┘           └───────┘      └────┘    └─┘
typ         └─┘  └──────┘          └───────┘     └────┘   └─┘ 
doc                                 └───────┘      └────┘    └─┘
529  begin
st   └─────
530    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
531    { show ite _ _ _ ∈ _,
id            └─┘       
src      └───┘└─┘└─────┘└┘
typ      └───┘└─┘└─────┘└┘
doc      └───┘   └─────┘ └┘
txt      └───┘   └─────┘ └┘
par      └───┘   └─────┘ └┘
pid      └───┘   └─────┘ └┘
st   ───┘└────────────────┘└─
532      split_ifs,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
st   ────────────┘└─
533      { intros a ha, exact top_le_iff.2 (set.mem_singleton_iff.1 (h ha)) },
id                            └────────┘    └───────────────────┘     └┘
src        └─────────┘  └────┘└────────┘└─┘ └───────────────────┘└─┘    └─┘
typ        └─────────┘  └────┘└────────┘└─┘ └───────────────────┘└─┘ └┘└─┘
doc        └─────────┘  └────┘          └─┘                      └─┘    └─┘
txt        └─────────┘  └────┘          └─┘                      └─┘    └─┘
par        └─────────┘  └────┘          └─┘                      └─┘    └─┘
pid              └───┘                 └─┘                      └─┘    └┘
st   ─────┘└─────────┘└────────────────────────────────────────────────────┘└┘
534      { rintro (⟨⟩|a) ha,
src        └──────────────┘
typ        └──────────────┘
doc        └──────────────┘
txt        └──────────────┘
par        └──────────────┘
pid              └────────┘
st   ─────────────────────┘└─
535        { exact le_top },
id                 └────┘
src          └────┘└────┘
typ          └────┘└────┘
doc          └────┘      
txt          └────┘      
par          └────┘      
pid                     
st   ───────┘└───────────┘└┘
536        refine some_le_some.2 (cInf_le _ ha),
id                └──────────┘    └─────┘   └┘
src        └─────┘└──────────┘└─┘ └─────┘└─┘  
typ        └─────┘└──────────┘└─┘ └─────┘└─┘└┘
doc        └─────┘            └─┘        └─┘  
txt        └─────┘            └─┘        └─┘  
par        └─────┘            └─┘        └─┘  
pid                          └─┘        └─┘  
st   ─────────────────────────────────────────┘└─
537        rcases hs with ⟨⟨⟩|b, hb⟩,
id                └┘
src        └─────┘  └──────────────┘
typ        └─────┘└┘└──────────────┘
doc        └─────┘  └──────────────┘
txt        └─────┘  └──────────────┘
par        └─────┘  └──────────────┘
pid                └──────────────┘
st   ──────────────────────────────┘└─
538        { exfalso,
src          └─────┘
typ          └─────┘
doc          └─────┘
txt          └─────┘
par          └─────┘
st   ───────┘└─────┘└─
539          apply h,
src          └────┘
typ          └────┘
doc          └────┘
txt          └────┘
par          └────┘
pid               
st   ──────────────┘└─
540          intros c hc,
src          └─────────┘
typ          └─────────┘
doc          └─────────┘
txt          └─────────┘
par          └─────────┘
pid                └───┘
st   ──────────────────┘└─
541          rw [mem_singleton_iff, ←top_le_iff],
id               └───────────────┘   └────────┘
src          └──┘└───────────────┘└─┘└────────┘
typ          └──┘└───────────────┘└─┘└────────┘
doc          └──┘                 └─┘          
txt          └──┘                 └─┘          
par          └──┘                 └─┘          
pid            └┘                 └─┘          
st   ────────────────────────────┘└───────────┘└──
542          exact hb hc },
id                 └┘ └┘
src          └────┘    
typ          └────┘└┘└┘
doc          └────┘    
txt          └────┘    
par          └────┘    
pid                   
st   ───────────────────┘└┘
543        use b,
id             
src        └──┘
typ        └──┘
doc        └──┘
txt        └──┘
par        └──┘
pid           
st   ──────────┘└─
544        intros c hc,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid              └───┘
st   ────────────────┘└─
545        exact some_le_some.1 (hb hc) } },
id               └──────────┘    └┘ └┘
src        └────┘└──────────┘└─┘     └┘
typ        └────┘└──────────┘└─┘ └┘└┘└┘
doc        └────┘            └─┘     └┘
txt        └────┘            └─┘     └┘
par        └────┘            └─┘     └┘
pid                         └─┘     
st   ──────────────────────────────────┘└──┘
546    { show ite _ _ _ ∈ _,
id            └─┘
src      └───┘└─┘└─────┘ └┘
typ      └───┘└─┘└─────┘ └┘
doc      └───┘   └─────┘ └┘
txt      └───┘   └─────┘ └┘
par      └───┘   └─────┘ └┘
pid      └───┘   └─────┘ └┘
st   ─────────────────────┘└─
547      split_ifs,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
st   ────────────┘└─
548      { intros _ _, exact le_top },
id                           └────┘
src        └────────┘  └────┘└────┘
typ        └────────┘  └────┘└────┘
doc        └────────┘  └────┘      
txt        └────────┘  └────┘      
par        └────────┘  └────┘      
pid              └──┘             
st   ─────┘└────────┘└─────────────┘└┘
549      { rintro (⟨⟩|a) ha,
src        └──────────────┘
typ        └──────────────┘
doc        └──────────────┘
txt        └──────────────┘
par        └──────────────┘
pid              └────────┘
st   ─────────────────────┘└─
550        { exfalso, apply h, intros b hb, exact set.mem_singleton_iff.2 (top_le_iff.1 (ha hb)) },
id                                                └───────────────────┘    └────────┘    └┘ └┘
src          └─────┘  └────┘   └─────────┘  └────┘└───────────────────┘└─┘ └────────┘└─┘     └─┘
typ          └─────┘  └────┘   └─────────┘  └────┘└───────────────────┘└─┘ └────────┘└─┘ └┘└┘└─┘
doc          └─────┘  └────┘   └─────────┘  └────┘                     └─┘           └─┘     └─┘
txt          └─────┘  └────┘   └─────────┘  └────┘                     └─┘           └─┘     └─┘
par          └─────┘  └────┘   └─────────┘  └────┘                     └─┘           └─┘     └─┘
pid                                 └───┘                            └─┘           └─┘     └┘
st   ───────┘└─────┘└───────┘└───────────┘└─────────────────────────────────────────────────────┘└┘
551        { refine some_le_some.2 (le_cInf _ _),
id                  └──────────┘    └─────┘
src          └─────┘└──────────┘└─┘ └─────┘└───┘
typ          └─────┘└──────────┘└─┘ └─────┘└───┘
doc          └─────┘            └─┘        └───┘
txt          └─────┘            └─┘        └───┘
par          └─────┘            └─┘        └───┘
pid                            └─┘        └───┘
st   ──────────────────────────────────────────┘└─
552          { classical, contrapose! h,
src            └───────┘  └───────────┘
typ            └───────┘  └───────────┘
doc            └───────┘  └───────────┘
txt            └───────┘  └───────────┘
par            └───────┘  └───────────┘
pid                                 └┘
st   ─────────┘└───────┘└─────────────┘└─
553            rintros (⟨⟩|a) ha,
src            └───────────────┘
typ            └───────────────┘
doc            └───────────────┘
txt            └───────────────┘
par            └───────────────┘
pid                   └────────┘
st   ──────────────────────────┘└─
554            { exact mem_singleton ⊤ },
id                     └───────────┘ 
src              └────┘└───────────┘
typ              └────┘└───────────┘
doc              └────┘              
txt              └────┘              
par              └────┘              
pid                                 
st   ───────────┘└────────────────────┘└┘
555            { exact (h ⟨a, ha⟩).elim }},
id                          └┘
src              └────┘    └┘  └──────┘
typ              └────┘  └┘└┘└──────┘
doc              └────┘    └┘  └──────┘
txt              └────┘    └┘  └──────┘
par              └────┘    └┘  └──────┘
pid                       └┘  └────┘└┘
st   ──────────────────────────────────┘└─┘
556          { intros b hb,
src            └─────────┘
typ            └─────────┘
doc            └─────────┘
txt            └─────────┘
par            └─────────┘
pid                  └───┘
st   ────────────────────┘└─
557            rw ←some_le_some,
id                 └──────────┘
src            └──┘└──────────┘
typ            └──┘└──────────┘
doc            └──┘
txt            └──┘
par            └──┘
pid              └┘
st   ─────────────────────────┘└─
558            exact ha hb } } } }
id                   └┘ └┘
src            └────┘    
typ            └────┘└┘└┘
doc            └────┘    
txt            └────┘    
par            └────┘    
pid                     
st   ─────────────────────┘└───────
559  end
st   ──┘
560  
561  lemma is_glb_Inf (s : set (with_top α)) : is_glb s (Inf s) :=
id                         └─┘  └──────┘      └────┘   └─┘ 
src                        └─┘  └──────┘       └────┘    └─┘
typ                        └─┘  └──────┘      └────┘   └─┘ 
doc                                            └────┘    └─┘
562  begin
st   └─────
563    by_cases hs : bdd_below s,
id                   └───────┘ 
src    └───────┘  └─┘└───────┘
typ    └───────┘  └─┘└───────┘
doc    └───────┘  └─┘└───────┘
txt    └───────┘  └─┘         
par    └───────┘  └─┘         
pid              └─┘         
st   ──────────────────────────┘└─
564    { exact is_glb_Inf' hs },
id             └─────────┘ └┘
src      └────┘└─────────┘  
typ      └────┘└─────────┘└┘
doc      └────┘└─────────┘  
txt      └────┘             
par      └────┘             
pid                        
st   ───┘└───────────────────┘└┘
565    { exfalso, apply hs, use ⊥, intros _ _, exact bot_le },
id                                                  └────┘
src      └─────┘  └────┘    └──┘  └────────┘  └────┘└────┘
typ      └─────┘  └────┘    └──┘  └────────┘  └────┘└────┘
doc      └─────┘  └────┘    └──┘   └────────┘  └────┘      
txt      └─────┘  └────┘    └──┘   └────────┘  └────┘      
par      └─────┘  └────┘    └──┘   └────────┘  └────┘      
pid                                    └──┘             
st   ──────────┘└────────┘└─────┘└──────────┘└─────────────┘└──
566  end
st   ──┘
567  
568  noncomputable instance : complete_linear_order (with_top α) :=
id                            └───────────────────┘  └──────┘ 
src                           └───────────────────┘  └──────┘
typ                           └───────────────────┘  └──────┘ 
doc                           └───────────────────┘
569  { Sup := Sup, le_Sup := assume s, (is_lub_Sup s).1, Sup_le := assume s, (is_lub_Sup s).2,
id            └─┘                      └────────┘                         └────────┘  
src           └─┘                       └────────┘                           └────────┘   
typ           └─┘                      └────────┘                         └────────┘  
doc           └─┘
570    Inf := Inf, le_Inf := assume s, (is_glb_Inf s).2, Inf_le := assume s, (is_glb_Inf s).1,
id            └─┘                      └────────┘                         └────────┘  
src           └─┘                       └────────┘                           └────────┘   
typ           └─┘                      └────────┘                         └────────┘  
doc           └─┘
571    decidable_le := classical.dec_rel _,
id                     └───────────────┘
src                    └───────────────┘
typ                    └───────────────┘
572    .. with_top.linear_order, ..with_top.lattice, ..with_top.order_top, ..with_top.order_bot }
id        └───────────────────┘    └──────────────┘    └────────────────┘    └────────────────┘
src       └───────────────────┘    └──────────────┘    └────────────────┘    └────────────────┘
typ       └───────────────────┘    └──────────────┘    └────────────────┘    └────────────────┘
573  
574  lemma coe_Sup {s : set α} (hb : bdd_above s) : (↑(Sup s) : with_top α) = (⨆a∈s, ↑a) :=
id                      └─┘         └───────┘       └─┘     └──────┘       
src                     └─┘          └───────┘        └─┘      └──────┘          
typ                     └─┘         └───────┘       └─┘     └──────┘       
doc                                  └───────┘         └─┘                        
575  begin
st   └─────
576    cases s.eq_empty_or_nonempty with hs hs,
id           └────────────────────┘
src    └────┘└────────────────────┘└─────────┘
typ    └────┘└────────────────────┘└─────────┘
doc    └────┘                      └─────────┘
txt    └────┘                      └─────────┘
par    └────┘                      └─────────┘
pid                               └─────────┘
st   ────────────────────────────────────────┘└─
577    { rw [hs, cSup_empty], simp only [set.mem_empty_eq, lattice.supr_bot, lattice.supr_false], refl },
id           └┘  └────────┘              └──────────────┘  └──────────────┘  └────────────────┘
src      └──┘  └┘└────────┘  └─────────┘└──────────────┘└┘└──────────────┘└┘└────────────────┘  └───┘
typ      └──┘└┘└┘└────────┘  └─────────┘└──────────────┘└┘└──────────────┘└┘└────────────────┘  └───┘
doc      └──┘  └┘            └─────────┘                └┘                └┘                    └───┘
txt      └──┘  └┘            └─────────┘                └┘                └┘                    └───┘
par      └──┘  └┘            └─────────┘                └┘                └┘                    └───┘
pid        └┘  └┘                └──┘└┘                └┘                └┘                        
st   ───┘└────┘└──────────┘└──────────────────────────────────────────────────────────────────┘└─────┘└┘
578    apply le_antisymm,
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────┘└─
579    { refine ((coe_le_iff _ _).2 $ assume b hb, cSup_le hs $ assume a has, coe_le_coe.1 $ hb ▸ _),
id                └────────┘                       └─────┘ └┘                 └────────┘        
src      └─────┘  └────────┘└──────┘       └─────┘└─────┘         └──────┘└────────┘└─┘   └─┘
typ      └─────┘  └────────┘└──────┘       └─────┘└─────┘└┘       └──────┘└────────┘└─┘   └─┘
doc      └─────┘            └──────┘       └─────┘                └──────┘          └─┘    └─┘
txt      └─────┘            └──────┘       └─────┘                └──────┘          └─┘    └─┘
par      └─────┘            └──────┘       └─────┘                └──────┘          └─┘    └─┘
pid                        └──────┘       └─────┘                └──────┘          └─┘    └─┘
st   ───┘└─────────────────────────────────────────────────────────────────────────────────────────┘└─
580      exact (le_supr_of_le a $ le_supr_of_le has $ _root_.le_refl _) },
id                               └───────────┘ └─┘   └────────────┘
src      └────┘                └───────────┘    └────────────┘└──┘
typ      └────┘               └───────────┘└─┘ └────────────┘└──┘
doc      └────┘                                               └──┘
txt      └────┘                                               └──┘
par      └────┘                                               └──┘
pid                                                          └─┘
st   ──────────────────────────────────────────────────────────────────┘└┘
581    { exact (supr_le $ assume a, supr_le $ assume ha, coe_le_coe.2 $ le_cSup hb ha) }
id                                  └─────┘              └────────┘     └─────┘ └┘
src      └────┘               └──┘└─────┘       └───┘└────────┘└─┘ └─────┘    └┘
typ      └────┘               └──┘└─────┘       └───┘└────────┘└─┘ └─────┘└┘  └┘
doc      └────┘               └──┘              └───┘          └─┘            └┘
txt      └────┘               └──┘              └───┘          └─┘            └┘
par      └────┘               └──┘              └───┘          └─┘            └┘
pid                          └──┘              └───┘          └─┘            
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
582  end
st   ──┘
583  
584  lemma coe_Inf {s : set α} (hs : s.nonempty) : (↑(Inf s) : with_top α) = (⨅a∈s, ↑a) :=
id                      └─┘         └───────┘      └─┘     └──────┘       
src                     └─┘           └───────┘      └─┘      └──────┘          
typ                     └─┘         └───────┘      └─┘     └──────┘       
doc                                   └───────┘       └─┘                        
585  let ⟨x, hx⟩ := hs in
id   └─┘    └┘     └┘
typ  └─┘    └┘     └┘
586  have (⨅a∈s, ↑a : with_top α) ≤ x, from infi_le_of_le x $ infi_le_of_le hx $ _root_.le_refl _,
id              └──────┘            └───────────┘     └───────────┘      └────────────┘
src                └──────┘             └───────────┘     └───────────┘      └────────────┘
typ             └──────┘            └───────────┘     └───────────┘      └────────────┘
doc           
587  let ⟨r, r_eq, hr⟩ := (le_coe_iff _ _).1 this in
id   └─┘                   └────────┘       └──┘
src                        └────────┘     
typ  └─┘                   └────────┘       └──┘
588  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
589    (le_infi $ assume a, le_infi $ assume ha, coe_le_coe.2 $ cInf_le (bdd_below_bot s) ha)
id      └─────┘            └─────┘          └┘  └────────┘    └─────┘  └───────────┘   └┘
src     └─────┘             └─────┘              └────────┘    └─────┘  └───────────┘
typ     └─────┘            └─────┘          └┘  └────────┘    └─────┘  └───────────┘   └┘
doc                                                                      └───────────┘
590    begin
st     └─────
591      refine (r_eq.symm ▸ coe_le_coe.2 $ le_cInf hs $ assume a has, coe_le_coe.1 $ _),
id               └───────┘                 └─────┘ └┘                 └────────┘
src      └─────┘ └───────┘          └─┘ └─────┘         └──────┘└────────┘└─┘ └─┘
typ      └─────┘ └───────┘          └─┘ └─────┘└┘       └──────┘└────────┘└─┘ └─┘
doc      └─────┘                     └─┘                 └──────┘          └─┘ └─┘
txt      └─────┘                     └─┘                 └──────┘          └─┘ └─┘
par      └─────┘                     └─┘                 └──────┘          └─┘ └─┘
pid                                 └─┘                 └──────┘          └─┘ └─┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
592      refine (r_eq ▸ infi_le_of_le a _),
id               └──┘   └───────────┘ 
src      └─────┘      └───────────┘ └─┘
typ      └─────┘ └──┘ └───────────┘└─┘
doc      └─────┘                    └─┘
txt      └─────┘                    └─┘
par      └─────┘                    └─┘
pid                                └─┘
st   ────────────────────────────────────┘└─
593      exact (infi_le_of_le has $ _root_.le_refl _),
id              └───────────┘ └─┘   └────────────┘
src      └────┘ └───────────┘    └────────────┘└─┘
typ      └────┘ └───────────┘└─┘ └────────────┘└─┘
doc      └────┘                                └─┘
txt      └────┘                                └─┘
par      └────┘                                └─┘
pid                                           └─┘
st   ───────────────────────────────────────────────┘└─
594    end
st   ────┘
595  
596  end with_top
597  
598  namespace enat
599  open_locale classical
600  open lattice
601  
602  noncomputable instance : complete_linear_order enat :=
id                            └───────────────────┘ └──┘
src                           └───────────────────┘ └──┘
typ                           └───────────────────┘ └──┘
doc                           └───────────────────┘
603  { Sup := λ s, with_top_equiv.symm $ Sup (with_top_equiv '' s),
id                └────────────┘└───┘   └─┘  └────────────┘ └┘ 
src                └────────────┘└───┘   └─┘  └────────────┘ └┘
typ               └────────────┘└───┘   └─┘  └────────────┘ └┘ 
doc                └────────────┘        └─┘  └────────────┘
604    Inf := λ s, with_top_equiv.symm $ Inf (with_top_equiv '' s),
id                └────────────┘└───┘   └─┘  └────────────┘ └┘ 
src                └────────────┘└───┘   └─┘  └────────────┘ └┘
typ               └────────────┘└───┘   └─┘  └────────────┘ └┘ 
doc                └────────────┘        └─┘  └────────────┘
605    le_Sup := by intros; rw ← with_top_equiv_le; simp; apply le_Sup _; simpa,
id                               └───────────────┘              └────┘
src                 └────┘  └───┘└───────────────┘  └──┘  └────┘└────┘└┘  └───┘
typ                 └────┘  └───┘└───────────────┘  └──┘  └────┘└────┘└┘  └───┘
doc                 └────┘  └───┘                   └──┘  └────┘      └┘  └───┘
txt                 └────┘  └───┘                   └──┘  └────┘      └┘  └───┘
par                 └────┘  └───┘                   └──┘  └────┘      └┘  └───┘
pid                           └─┘                                    └┘
st                 └──────────────────────────────────────────────────────────┘
606    Inf_le := by intros; rw ← with_top_equiv_le; simp; apply Inf_le _; simpa,
id                               └───────────────┘              └────┘
src                 └────┘  └───┘└───────────────┘  └──┘  └────┘└────┘└┘  └───┘
typ                 └────┘  └───┘└───────────────┘  └──┘  └────┘└────┘└┘  └───┘
doc                 └────┘  └───┘                   └──┘  └────┘      └┘  └───┘
txt                 └────┘  └───┘                   └──┘  └────┘      └┘  └───┘
par                 └────┘  └───┘                   └──┘  └────┘      └┘  └───┘
pid                           └─┘                                    └┘
st                 └──────────────────────────────────────────────────────────┘
607    Sup_le := begin
st               └─────
608      intros s a h1,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid            └─────┘
st   ────────────────┘└─
609      rw [← with_top_equiv_le, with_top_equiv.right_inverse_symm],
id             └───────────────┘
src      └────┘└───────────────┘└┘                                 
typ      └────┘└───────────────┘└┘└───────────────────────────────┘
doc      └────┘                 └┘                                 
txt      └────┘                 └┘                                 
par      └────┘                 └┘                                 
pid        └──┘                 └┘                                 
st   ──────────────────────────┘└─────────────────────────────────┘└──
610      apply Sup_le _,
id             └────┘
src      └────┘└────┘└┘
typ      └────┘└────┘└┘
doc      └────┘      └┘
txt      └────┘      └┘
par      └────┘      └┘
pid                 └┘
st   ─────────────────┘└─
611      rintros b ⟨x, h2, rfl⟩,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid             └─────────────┘
st   ─────────────────────────┘└─
612      rw with_top_equiv_le,
id          └───────────────┘
src      └─┘└───────────────┘
typ      └─┘└───────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────────────┘└─
613      apply h1,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
614      assumption
src      └──────────
typ      └──────────
doc      └──────────
txt      └──────────
par      └──────────
pid                
st   ───────────────
615    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
616    le_Inf := begin
st               └─────
617      intros s a h1,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid            └─────┘
st   ────────────────┘└─
618      rw [← with_top_equiv_le, with_top_equiv.right_inverse_symm],
id             └───────────────┘
src      └────┘└───────────────┘└┘                                 
typ      └────┘└───────────────┘└┘└───────────────────────────────┘
doc      └────┘                 └┘                                 
txt      └────┘                 └┘                                 
par      └────┘                 └┘                                 
pid        └──┘                 └┘                                 
st   ──────────────────────────┘└─────────────────────────────────┘└──
619      apply le_Inf _,
id             └────┘
src      └────┘└────┘└┘
typ      └────┘└────┘└┘
doc      └────┘      └┘
txt      └────┘      └┘
par      └────┘      └┘
pid                 └┘
st   ─────────────────┘└─
620      rintros b ⟨x, h2, rfl⟩,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid             └─────────────┘
st   ─────────────────────────┘└─
621      rw with_top_equiv_le,
id          └───────────────┘
src      └─┘└───────────────┘
typ      └─┘└───────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────────────┘└─
622      apply h1,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
623      assumption
src      └──────────
typ      └──────────
doc      └──────────
txt      └──────────
par      └──────────
pid                
st   ───────────────
624    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
625    ..enat.decidable_linear_order,
id       └─────────────────────────┘
src      └─────────────────────────┘
typ      └─────────────────────────┘
626    ..enat.lattice.bounded_lattice }
id       └──────────────────────────┘
src      └──────────────────────────┘
typ      └──────────────────────────┘
627  
628  end enat
629  
630  section order_dual
631  open lattice
632  
633  instance (α : Type*) [conditionally_complete_lattice α] :
id                         └────────────────────────────┘ 
src                        └────────────────────────────┘
typ                        └────────────────────────────┘ 
doc                        └────────────────────────────┘
634    conditionally_complete_lattice (order_dual α) :=
id     └────────────────────────────┘  └────────┘ 
src    └────────────────────────────┘  └────────┘
typ    └────────────────────────────┘  └────────┘ 
doc    └────────────────────────────┘  └────────┘
635  { le_cSup := @cInf_le α _,
id                 └─────┘ 
src                └─────┘
typ                └─────┘ 
636    cSup_le := @le_cInf α _,
id                 └─────┘ 
src                └─────┘
typ                └─────┘ 
637    le_cInf := @cSup_le α _,
id                 └─────┘ 
src                └─────┘
typ                └─────┘ 
638    cInf_le := @le_cSup α _,
id                 └─────┘ 
src                └─────┘
typ                └─────┘ 
639    ..order_dual.lattice.has_Inf α,
id       └────────────────────────┘ 
src      └────────────────────────┘
typ      └────────────────────────┘ 
640    ..order_dual.lattice.has_Sup α,
id       └────────────────────────┘ 
src      └────────────────────────┘
typ      └────────────────────────┘ 
641    ..order_dual.lattice.lattice α }
id       └────────────────────────┘ 
src      └────────────────────────┘
typ      └────────────────────────┘ 
642  
643  instance (α : Type*) [conditionally_complete_linear_order α] :
id                         └─────────────────────────────────┘ 
src                        └─────────────────────────────────┘
typ                        └─────────────────────────────────┘ 
644    conditionally_complete_linear_order (order_dual α) :=
id     └─────────────────────────────────┘  └────────┘ 
src    └─────────────────────────────────┘  └────────┘
typ    └─────────────────────────────────┘  └────────┘ 
doc                                         └────────┘
645  { ..order_dual.lattice.conditionally_complete_lattice α,
id       └───────────────────────────────────────────────┘ 
src      └───────────────────────────────────────────────┘
typ      └───────────────────────────────────────────────┘ 
646    ..order_dual.decidable_linear_order α }
id       └───────────────────────────────┘ 
src      └───────────────────────────────┘
typ      └───────────────────────────────┘ 
647  
648  end order_dual
649  
650  section with_top_bot
651  
652  /-! ### Complete lattice structure on `with_top (with_bot α)`
653  
654  If `α` is a `conditionally_complete_lattice`, then we show that `with_top α` and `with_bot α`
655  also inherit the structure of conditionally complete lattices. Furthermore, we show
656  that `with_top (with_bot α)` naturally inherits the structure of a complete lattice. Note that
657  for α a conditionally complete lattice, `Sup` and `Inf` both return junk values
658  for sets which are empty or unbounded. The extension of `Sup` to `with_top α` fixes
659  the unboundedness problem and the extension to `with_bot α` fixes the problem with
660  the empty set.
661  
662  This result can be used to show that the extended reals [-∞, ∞] are a complete lattice.
663  -/
664  
665  open lattice
666  
667  open_locale classical
668  
669  /-- Adding a top element to a conditionally complete lattice gives a conditionally complete lattice -/
670  noncomputable instance with_top.conditionally_complete_lattice
671    {α : Type*} [conditionally_complete_lattice α] :
id                  └────────────────────────────┘ 
src                 └────────────────────────────┘
typ                 └────────────────────────────┘ 
doc                 └────────────────────────────┘
672    conditionally_complete_lattice (with_top α) :=
id     └────────────────────────────┘  └──────┘ 
src    └────────────────────────────┘  └──────┘
typ    └────────────────────────────┘  └──────┘ 
doc    └────────────────────────────┘
673  { le_cSup := λ S a hS haS, (with_top.is_lub_Sup' ⟨a, haS⟩).1 haS,
id                    └┘ └─┘   └──────────────────┘    └─┘    └─┘
src                              └──────────────────┘          
typ                   └┘ └─┘   └──────────────────┘    └─┘    └─┘
doc                              └──────────────────┘
674    cSup_le := λ S a hS haS, (with_top.is_lub_Sup' hS).2 haS,
id                    └┘ └─┘   └──────────────────┘ └┘   └─┘
src                              └──────────────────┘    
typ                   └┘ └─┘   └──────────────────┘ └┘   └─┘
doc                              └──────────────────┘
675    cInf_le := λ S a hS haS, (with_top.is_glb_Inf' hS).1 haS,
id                    └┘ └─┘   └──────────────────┘ └┘   └─┘
src                              └──────────────────┘    
typ                   └┘ └─┘   └──────────────────┘ └┘   └─┘
doc                              └──────────────────┘
676    le_cInf := λ S a hS haS, (with_top.is_glb_Inf' ⟨a, haS⟩).2 haS,
id                    └┘ └─┘   └──────────────────┘    └─┘    └─┘
src                              └──────────────────┘          
typ                   └┘ └─┘   └──────────────────┘    └─┘    └─┘
doc                              └──────────────────┘
677    ..with_top.lattice,
id       └──────────────┘
src      └──────────────┘
typ      └──────────────┘
678    ..with_top.lattice.has_Sup,
id       └──────────────────────┘
src      └──────────────────────┘
typ      └──────────────────────┘
679    ..with_top.lattice.has_Inf }
id       └──────────────────────┘
src      └──────────────────────┘
typ      └──────────────────────┘
680  
681  /-- Adding a bottom element to a conditionally complete lattice gives a conditionally complete lattice -/
682  noncomputable instance with_bot.conditionally_complete_lattice
683    {α : Type*} [conditionally_complete_lattice α] :
id                  └────────────────────────────┘ 
src                 └────────────────────────────┘
typ                 └────────────────────────────┘ 
doc                 └────────────────────────────┘
684    conditionally_complete_lattice (with_bot α) :=
id     └────────────────────────────┘  └──────┘ 
src    └────────────────────────────┘  └──────┘
typ    └────────────────────────────┘  └──────┘ 
doc    └────────────────────────────┘
685  { le_cSup := (@with_top.conditionally_complete_lattice (order_dual α) _).cInf_le,
id                  └─────────────────────────────────────┘  └────────┘     └─────┘
src                 └─────────────────────────────────────┘  └────────┘      └─────┘
typ                 └─────────────────────────────────────┘  └────────┘     └─────┘
doc                 └─────────────────────────────────────┘  └────────┘
686    cSup_le := (@with_top.conditionally_complete_lattice (order_dual α) _).le_cInf,
id                  └─────────────────────────────────────┘  └────────┘     └─────┘
src                 └─────────────────────────────────────┘  └────────┘      └─────┘
typ                 └─────────────────────────────────────┘  └────────┘     └─────┘
doc                 └─────────────────────────────────────┘  └────────┘
687    cInf_le := (@with_top.conditionally_complete_lattice (order_dual α) _).le_cSup,
id                  └─────────────────────────────────────┘  └────────┘     └─────┘
src                 └─────────────────────────────────────┘  └────────┘      └─────┘
typ                 └─────────────────────────────────────┘  └────────┘     └─────┘
doc                 └─────────────────────────────────────┘  └────────┘
688    le_cInf := (@with_top.conditionally_complete_lattice (order_dual α) _).cSup_le,
id                  └─────────────────────────────────────┘  └────────┘     └─────┘
src                 └─────────────────────────────────────┘  └────────┘      └─────┘
typ                 └─────────────────────────────────────┘  └────────┘     └─────┘
doc                 └─────────────────────────────────────┘  └────────┘
689    ..with_bot.lattice,
id       └──────────────┘
src      └──────────────┘
typ      └──────────────┘
690    ..with_bot.lattice.has_Sup,
id       └──────────────────────┘
src      └──────────────────────┘
typ      └──────────────────────┘
691    ..with_bot.lattice.has_Inf }
id       └──────────────────────┘
src      └──────────────────────┘
typ      └──────────────────────┘
692  
693  /-- Adding a bottom and a top to a conditionally complete lattice gives a bounded lattice-/
694  noncomputable instance {α : Type*} [conditionally_complete_lattice α] : bounded_lattice (with_top (with_bot α)) :=
id                                       └────────────────────────────┘     └─────────────┘  └──────┘  └──────┘ 
src                                      └────────────────────────────┘      └─────────────┘  └──────┘  └──────┘
typ                                      └────────────────────────────┘     └─────────────┘  └──────┘  └──────┘ 
doc                                      └────────────────────────────┘      └─────────────┘
695  { ..with_top.order_bot,
id       └────────────────┘
src      └────────────────┘
typ      └────────────────┘
696    ..with_top.order_top,
id       └────────────────┘
src      └────────────────┘
typ      └────────────────┘
697    ..conditionally_complete_lattice.to_lattice _ }
id       └───────────────────────────────────────┘
src      └───────────────────────────────────────┘
typ      └───────────────────────────────────────┘
698  
699  theorem with_bot.cSup_empty {α : Type*} [conditionally_complete_lattice α] :
id                                            └────────────────────────────┘ 
src                                           └────────────────────────────┘
typ                                           └────────────────────────────┘ 
doc                                           └────────────────────────────┘
700    Sup (∅ : set (with_bot α)) = ⊥ :=
id     └─┘     └─┘  └──────┘     
src    └─┘     └─┘  └──────┘      
typ    └─┘     └─┘  └──────┘     
doc    └─┘
701  begin
st   └─────
702    show ite _ _ _ = ⊥,
id          └─┘        
src    └───┘└─┘└─────┘
typ    └───┘└─┘└─────┘
doc    └───┘   └─────┘ 
txt    └───┘   └─────┘ 
par    └───┘   └─────┘ 
pid    └───┘   └─────┘ 
st   ───────────────────┘└─
703    split_ifs; finish,
src    └───────┘  └────┘
typ    └───────┘  └────┘
doc    └───────┘  └────┘
txt    └───────┘  └────┘
par    └───────┘  └────┘
st   ──────────────────┘└─
704  end
st   ──┘
705  
706  noncomputable instance {α : Type*} [conditionally_complete_lattice α] :
id                                       └────────────────────────────┘ 
src                                      └────────────────────────────┘
typ                                      └────────────────────────────┘ 
doc                                      └────────────────────────────┘
707    complete_lattice (with_top (with_bot α)) :=
id     └──────────────┘  └──────┘  └──────┘ 
src    └──────────────┘  └──────┘  └──────┘
typ    └──────────────┘  └──────┘  └──────┘ 
doc    └──────────────┘
708  { le_Sup := λ S a haS, (with_top.is_lub_Sup' ⟨a, haS⟩).1 haS,
id                   └─┘   └──────────────────┘    └─┘    └─┘
src                          └──────────────────┘          
typ                  └─┘   └──────────────────┘    └─┘    └─┘
doc                          └──────────────────┘
709    Sup_le := λ S a ha,
id                   └┘
typ                  └┘
710      begin
st       └─────
711        cases S.eq_empty_or_nonempty with h,
id               └────────────────────┘
src        └────┘└────────────────────┘└─────┘
typ        └────┘└────────────────────┘└─────┘
doc        └────┘                      └─────┘
txt        └────┘                      └─────┘
par        └────┘                      └─────┘
pid                                   └─────┘
st   ────────────────────────────────────────┘└─
712        { show ite _ _ _ ≤ a,
id                └─┘        
src          └───┘└─┘└─────┘
typ          └───┘└─┘└─────┘
doc          └───┘   └─────┘ 
txt          └───┘   └─────┘ 
par          └───┘   └─────┘ 
pid          └───┘   └─────┘ 
st   ───────┘└────────────────┘└─
713          split_ifs,
src          └───────┘
typ          └───────┘
doc          └───────┘
txt          └───────┘
par          └───────┘
st   ────────────────┘└─
714          { rw h at h_1, cases h_1 },
id                               └─┘
src            └─┘ └─────┘  └────┘   
typ            └─┘└─────┘  └────┘└─┘
doc            └─┘ └─────┘  └────┘   
txt            └─┘ └─────┘  └────┘   
par            └─┘ └─────┘  └────┘   
pid               └─────┘          
st   ─────────┘└─────────┘└──────────┘└┘
715          { convert bot_le, convert with_bot.cSup_empty, rw h, refl },
id                     └────┘          └─────────────────┘     
src            └──────┘└────┘  └──────┘└─────────────────┘  └─┘   └───┘
typ            └──────┘└────┘  └──────┘└─────────────────┘  └─┘  └───┘
doc            └──────┘        └──────┘                     └─┘   └───┘
txt            └──────┘        └──────┘                     └─┘   └───┘
par            └──────┘        └──────┘                     └─┘   └───┘
pid                                                                
st   ─────────┘└────────────┘└───────────────────────────┘└────┘└─────┘└┘
716          { exfalso, apply h_2, use ⊥, rw h, rintro b ⟨⟩ } },
id                                          
src            └─────┘  └────┘     └──┘  └─┘   └──────────┘
typ            └─────┘  └────┘     └──┘  └─┘  └──────────┘
doc            └─────┘  └────┘     └──┘   └─┘   └──────────┘
txt            └─────┘  └────┘     └──┘   └─┘   └──────────┘
par            └─────┘  └────┘     └──┘   └─┘   └──────────┘
pid                                                └───┘
st   ────────────────┘└─────────┘└─────┘└────┘└────────────┘└──┘
717        { refine (with_top.is_lub_Sup' h).2 ha }
id                   └──────────────────┘     └┘
src          └─────┘ └──────────────────┘ └──┘  
typ          └─────┘ └──────────────────┘└──┘└┘
doc          └─────┘ └──────────────────┘ └──┘  
txt          └─────┘                      └──┘  
par          └─────┘                      └──┘  
pid                                      └──┘  
st   ────────────────────────────────────────────┘└─
718      end,
st   ──────┘
719    Inf_le := λ S a haS,
id                   └─┘
typ                  └─┘
720      show ite _ _ _ ≤ a,
id            └─┘        
src           └─┘       
typ           └─┘        
721      begin
st       └─────
722        split_ifs,
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
st   ──────────────┘└─
723        { cases a with a, exact _root_.le_refl _,
id                                └────────────┘
src          └────┘ └─────┘  └────┘└────────────┘└┘
typ          └────┘└─────┘  └────┘└────────────┘└┘
doc          └────┘ └─────┘  └────┘              └┘
txt          └────┘ └─────┘  └────┘              └┘
par          └────┘ └─────┘  └────┘              └┘
pid                └─────┘                     └┘
st   ───────┘└────────────┘└──────────────────────┘└─
724          cases (h haS); tauto },
id                   └─┘
src          └────┘       └────┘
typ          └────┘ └─┘  └────┘
doc          └────┘       └────┘
txt          └────┘       └────┘
par          └────┘       └────┘
pid                           
st   ────────────────────────────┘└┘
725        { cases a,
id                 
src          └────┘
typ          └────┘
doc          └────┘
txt          └────┘
par          └────┘
pid               
st   ──────────────┘└─
726          { exact le_top },
id                   └────┘
src            └────┘└────┘
typ            └────┘└────┘
doc            └────┘      
txt            └────┘      
par            └────┘      
pid                       
st   ─────────┘└───────────┘└┘
727          { apply with_top.some_le_some.2, refine cInf_le _ haS, use ⊥, intros b hb, exact bot_le } }
id                   └───────────────────┘           └─────┘   └─┘                            └────┘
src            └────┘└───────────────────┘└┘  └─────┘└─────┘└─┘     └──┘   └─────────┘  └────┘└────┘
typ            └────┘└───────────────────┘└┘  └─────┘└─────┘└─┘└─┘  └──┘   └─────────┘  └────┘└────┘
doc            └────┘                     └┘  └─────┘       └─┘     └──┘   └─────────┘  └────┘      
txt            └────┘                     └┘  └─────┘       └─┘     └──┘   └─────────┘  └────┘      
par            └────┘                     └┘  └─────┘       └─┘     └──┘   └─────────┘  └────┘      
pid                                      └┘               └─┘                 └───┘             
st   ──────────────────────────────────────┘└────────────────────┘└─────┘└───────────┘└─────────────┘└───
728      end,
st   ──────┘
729    le_Inf := λ S a haS, (with_top.is_glb_Inf' ⟨a, haS⟩).2 haS,
id                   └─┘   └──────────────────┘    └─┘    └─┘
src                          └──────────────────┘          
typ                  └─┘   └──────────────────┘    └─┘    └─┘
doc                          └──────────────────┘
730    ..with_top.lattice.has_Inf,
id       └──────────────────────┘
src      └──────────────────────┘
typ      └──────────────────────┘
731    ..with_top.lattice.has_Sup,
id       └──────────────────────┘
src      └──────────────────────┘
typ      └──────────────────────┘
732    ..with_top.lattice.bounded_lattice }
id       └──────────────────────────────┘
src      └──────────────────────────────┘
typ      └──────────────────────────────┘
doc      └──────────────────────────────┘
733  
734  end with_top_bot